Theorem f1oiso 2942

Description: Any one-to-one onto function determines an isomorphism with an induced relation S. Proposition 6.33 of [TakeutiZaring] p. 34.

Assertion

Ref	Expression
f1oiso	⊢ ((H:A–1-1-onto→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) → H Isom R, S (A, B))

Distinct variable group(s):   x,y,z,w,A   x,B,y   x,H,y,z,w   x,R,y,z,w

Proof of Theorem f1oiso

Step	Hyp	Ref	Expression
1		pm3.26 256	. . 3 ⊢ ((H:A–1-1-onto→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) → H:A–1-1-onto→B)
2		eleq2 1150	. . . . . . . . . 10 ⊢ (S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)} → (⟨(H ‘v), (H ‘u)⟩ ∈ S ↔ ⟨(H ‘v), (H ‘u)⟩ ∈ {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}))
3		f1fveq 2918	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((H:A–1-1→B ∧ (v ∈ A ∧ x ∈ A)) → ((H ‘v) = (H ‘x) ↔ v = x))
4		cleqcom 1103	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (v = x ↔ x = v)
5	3, 4	syl6bb 414	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((H:A–1-1→B ∧ (v ∈ A ∧ x ∈ A)) → ((H ‘v) = (H ‘x) ↔ x = v))
6	5	anassrs 338	. . . . . . . . . . . . . . . . . . 19 ⊢ (((H:A–1-1→B ∧ v ∈ A) ∧ x ∈ A) → ((H ‘v) = (H ‘x) ↔ x = v))
7	6	anbi1d 469	. . . . . . . . . . . . . . . . . 18 ⊢ (((H:A–1-1→B ∧ v ∈ A) ∧ x ∈ A) → (((H ‘v) = (H ‘x) ∧ ((H ‘u) = (H ‘y) ∧ xRy)) ↔ (x = v ∧ ((H ‘u) = (H ‘y) ∧ xRy))))
8		anass 336	. . . . . . . . . . . . . . . . . 18 ⊢ ((((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy) ↔ ((H ‘v) = (H ‘x) ∧ ((H ‘u) = (H ‘y) ∧ xRy)))
9	7, 8	syl5bb 410	. . . . . . . . . . . . . . . . 17 ⊢ (((H:A–1-1→B ∧ v ∈ A) ∧ x ∈ A) → ((((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy) ↔ (x = v ∧ ((H ‘u) = (H ‘y) ∧ xRy))))
10	9	birexdv 1220	. . . . . . . . . . . . . . . 16 ⊢ (((H:A–1-1→B ∧ v ∈ A) ∧ x ∈ A) → (∃y ∈ A (((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy) ↔ ∃y ∈ A (x = v ∧ ((H ‘u) = (H ‘y) ∧ xRy))))
11		r19.42v 1303	. . . . . . . . . . . . . . . 16 ⊢ (∃y ∈ A (x = v ∧ ((H ‘u) = (H ‘y) ∧ xRy)) ↔ (x = v ∧ ∃y ∈ A ((H ‘u) = (H ‘y) ∧ xRy)))
12	10, 11	syl6bb 414	. . . . . . . . . . . . . . 15 ⊢ (((H:A–1-1→B ∧ v ∈ A) ∧ x ∈ A) → (∃y ∈ A (((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy) ↔ (x = v ∧ ∃y ∈ A ((H ‘u) = (H ‘y) ∧ xRy))))
13	12	birexdva 1216	. . . . . . . . . . . . . 14 ⊢ ((H:A–1-1→B ∧ v ∈ A) → (∃x ∈ A ∃y ∈ A (((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy) ↔ ∃x ∈ A (x = v ∧ ∃y ∈ A ((H ‘u) = (H ‘y) ∧ xRy))))
14		breq1 2065	. . . . . . . . . . . . . . . . . 18 ⊢ (x = v → (xRy ↔ vRy))
15	14	anbi2d 468	. . . . . . . . . . . . . . . . 17 ⊢ (x = v → (((H ‘u) = (H ‘y) ∧ xRy) ↔ ((H ‘u) = (H ‘y) ∧ vRy)))
16	15	birexdv 1220	. . . . . . . . . . . . . . . 16 ⊢ (x = v → (∃y ∈ A ((H ‘u) = (H ‘y) ∧ xRy) ↔ ∃y ∈ A ((H ‘u) = (H ‘y) ∧ vRy)))
17	16	ceqsrexv 1413	. . . . . . . . . . . . . . 15 ⊢ (v ∈ A → (∃x ∈ A (x = v ∧ ∃y ∈ A ((H ‘u) = (H ‘y) ∧ xRy)) ↔ ∃y ∈ A ((H ‘u) = (H ‘y) ∧ vRy)))
18	17	adantl 305	. . . . . . . . . . . . . 14 ⊢ ((H:A–1-1→B ∧ v ∈ A) → (∃x ∈ A (x = v ∧ ∃y ∈ A ((H ‘u) = (H ‘y) ∧ xRy)) ↔ ∃y ∈ A ((H ‘u) = (H ‘y) ∧ vRy)))
19	13, 18	bitrd 406	. . . . . . . . . . . . 13 ⊢ ((H:A–1-1→B ∧ v ∈ A) → (∃x ∈ A ∃y ∈ A (((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy) ↔ ∃y ∈ A ((H ‘u) = (H ‘y) ∧ vRy)))
20		f1fveq 2918	. . . . . . . . . . . . . . . . . 18 ⊢ ((H:A–1-1→B ∧ (u ∈ A ∧ y ∈ A)) → ((H ‘u) = (H ‘y) ↔ u = y))
21		cleqcom 1103	. . . . . . . . . . . . . . . . . 18 ⊢ (u = y ↔ y = u)
22	20, 21	syl6bb 414	. . . . . . . . . . . . . . . . 17 ⊢ ((H:A–1-1→B ∧ (u ∈ A ∧ y ∈ A)) → ((H ‘u) = (H ‘y) ↔ y = u))
23	22	anassrs 338	. . . . . . . . . . . . . . . 16 ⊢ (((H:A–1-1→B ∧ u ∈ A) ∧ y ∈ A) → ((H ‘u) = (H ‘y) ↔ y = u))
24	23	anbi1d 469	. . . . . . . . . . . . . . 15 ⊢ (((H:A–1-1→B ∧ u ∈ A) ∧ y ∈ A) → (((H ‘u) = (H ‘y) ∧ vRy) ↔ (y = u ∧ vRy)))
25	24	birexdva 1216	. . . . . . . . . . . . . 14 ⊢ ((H:A–1-1→B ∧ u ∈ A) → (∃y ∈ A ((H ‘u) = (H ‘y) ∧ vRy) ↔ ∃y ∈ A (y = u ∧ vRy)))
26		breq2 2066	. . . . . . . . . . . . . . . 16 ⊢ (y = u → (vRy ↔ vRu))
27	26	ceqsrexv 1413	. . . . . . . . . . . . . . 15 ⊢ (u ∈ A → (∃y ∈ A (y = u ∧ vRy) ↔ vRu))
28	27	adantl 305	. . . . . . . . . . . . . 14 ⊢ ((H:A–1-1→B ∧ u ∈ A) → (∃y ∈ A (y = u ∧ vRy) ↔ vRu))
29	25, 28	bitrd 406	. . . . . . . . . . . . 13 ⊢ ((H:A–1-1→B ∧ u ∈ A) → (∃y ∈ A ((H ‘u) = (H ‘y) ∧ vRy) ↔ vRu))
30	19, 29	sylan9bb 418	. . . . . . . . . . . 12 ⊢ (((H:A–1-1→B ∧ v ∈ A) ∧ (H:A–1-1→B ∧ u ∈ A)) → (∃x ∈ A ∃y ∈ A (((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy) ↔ vRu))
31	30	anandis 394	. . . . . . . . . . 11 ⊢ ((H:A–1-1→B ∧ (v ∈ A ∧ u ∈ A)) → (∃x ∈ A ∃y ∈ A (((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy) ↔ vRu))
32		fvex 2838	. . . . . . . . . . . 12 ⊢ (H ‘v) ∈ V
33		fvex 2838	. . . . . . . . . . . 12 ⊢ (H ‘u) ∈ V
34		cleq1 1107	. . . . . . . . . . . . . . . 16 ⊢ (z = (H ‘v) → (z = (H ‘x) ↔ (H ‘v) = (H ‘x)))
35	34	anbi1d 469	. . . . . . . . . . . . . . 15 ⊢ (z = (H ‘v) → ((z = (H ‘x) ∧ w = (H ‘y)) ↔ ((H ‘v) = (H ‘x) ∧ w = (H ‘y))))
36	35	anbi1d 469	. . . . . . . . . . . . . 14 ⊢ (z = (H ‘v) → (((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy) ↔ (((H ‘v) = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)))
37	36	birexdv 1220	. . . . . . . . . . . . 13 ⊢ (z = (H ‘v) → (∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy) ↔ ∃y ∈ A (((H ‘v) = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)))
38	37	birexdv 1220	. . . . . . . . . . . 12 ⊢ (z = (H ‘v) → (∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy) ↔ ∃x ∈ A ∃y ∈ A (((H ‘v) = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)))
39		cleq1 1107	. . . . . . . . . . . . . . . 16 ⊢ (w = (H ‘u) → (w = (H ‘y) ↔ (H ‘u) = (H ‘y)))
40	39	anbi2d 468	. . . . . . . . . . . . . . 15 ⊢ (w = (H ‘u) → (((H ‘v) = (H ‘x) ∧ w = (H ‘y)) ↔ ((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y))))
41	40	anbi1d 469	. . . . . . . . . . . . . 14 ⊢ (w = (H ‘u) → ((((H ‘v) = (H ‘x) ∧ w = (H ‘y)) ∧ xRy) ↔ (((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy)))
42	41	birexdv 1220	. . . . . . . . . . . . 13 ⊢ (w = (H ‘u) → (∃y ∈ A (((H ‘v) = (H ‘x) ∧ w = (H ‘y)) ∧ xRy) ↔ ∃y ∈ A (((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy)))
43	42	birexdv 1220	. . . . . . . . . . . 12 ⊢ (w = (H ‘u) → (∃x ∈ A ∃y ∈ A (((H ‘v) = (H ‘x) ∧ w = (H ‘y)) ∧ xRy) ↔ ∃x ∈ A ∃y ∈ A (((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy)))
44	32, 33, 38, 43	opelopab 2117	. . . . . . . . . . 11 ⊢ (⟨(H ‘v), (H ‘u)⟩ ∈ {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)} ↔ ∃x ∈ A ∃y ∈ A (((H ‘v) = (H ‘x) ∧ (H ‘u) = (H ‘y)) ∧ xRy))
45	31, 44	syl5bb 410	. . . . . . . . . 10 ⊢ ((H:A–1-1→B ∧ (v ∈ A ∧ u ∈ A)) → (⟨(H ‘v), (H ‘u)⟩ ∈ {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)} ↔ vRu))
46	2, 45	sylan9bbr 419	. . . . . . . . 9 ⊢ (((H:A–1-1→B ∧ (v ∈ A ∧ u ∈ A)) ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) → (⟨(H ‘v), (H ‘u)⟩ ∈ S ↔ vRu))
47	46	an1rs 373	. . . . . . . 8 ⊢ (((H:A–1-1→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) ∧ (v ∈ A ∧ u ∈ A)) → (⟨(H ‘v), (H ‘u)⟩ ∈ S ↔ vRu))
48		df-br 2063	. . . . . . . 8 ⊢ ((H ‘v)S(H ‘u) ↔ ⟨(H ‘v), (H ‘u)⟩ ∈ S)
49	47, 48	syl5rbb 411	. . . . . . 7 ⊢ (((H:A–1-1→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) ∧ (v ∈ A ∧ u ∈ A)) → (vRu ↔ (H ‘v)S(H ‘u)))
50	49	exp32 294	. . . . . 6 ⊢ ((H:A–1-1→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) → (v ∈ A → (u ∈ A → (vRu ↔ (H ‘v)S(H ‘u)))))
51	50	r19.21adv 1262	. . . . 5 ⊢ ((H:A–1-1→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) → (v ∈ A → ∀u ∈ A (vRu ↔ (H ‘v)S(H ‘u))))
52	51	r19.21aiv 1259	. . . 4 ⊢ ((H:A–1-1→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) → ∀v ∈ A ∀u ∈ A (vRu ↔ (H ‘v)S(H ‘u)))
53		f1of1 2799	. . . 4 ⊢ (H:A–1-1-onto→B → H:A–1-1→B)
54	52, 53	sylan 343	. . 3 ⊢ ((H:A–1-1-onto→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) → ∀v ∈ A ∀u ∈ A (vRu ↔ (H ‘v)S(H ‘u)))
55	1, 54	jca 236	. 2 ⊢ ((H:A–1-1-onto→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) → (H:A–1-1-onto→B ∧ ∀v ∈ A ∀u ∈ A (vRu ↔ (H ‘v)S(H ‘u))))
56		df-iso 2439	. 2 ⊢ (H Isom R, S (A, B) ↔ (H:A–1-1-onto→B ∧ ∀v ∈ A ∀u ∈ A (vRu ↔ (H ‘v)S(H ‘u))))
57	55, 56	sylibr 175	1 ⊢ ((H:A–1-1-onto→B ∧ S = {⟨z, w⟩∣∃x ∈ A ∃y ∈ A ((z = (H ‘x) ∧ w = (H ‘y)) ∧ xRy)}) → H Isom R, S (A, B))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   = weq 797   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  ⟨cop 1810   class class class wbr 2054  {copab 2055  –1-1→wf1 2419  –1-1-onto→wf1o 2421   ‘cfv 2422   Isom wiso 2423

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-f1o 2437  df-fv 2438  df-iso 2439

metamath.org