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>. | E.x e. A E.y e. 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>. | E.x e. A E.y e. A ((z = (H` x) /\ w = (H` y)) /\ xRy)}) -> H:A-1-1-onto->B)
2		eleq2 1150	. . . . . . . . . 10 |- (S = {<.z, w>. | E.x e. A E.y e. A ((z = (H` x) /\ w = (H` y)) /\ xRy)} -> (<.(H` v), (H` u)>. e. S <-> <.(H` v), (H` u)>. e. {<.z, w>. | E.x e. A E.y e. A ((z = (H` x) /\ w = (H` y)) /\ xRy)}))
3		f1fveq 2918	. . . . . . . . . . . . . . . . . . . . 21 |- ((H:A-1-1->B /\ (v e. A /\ x e. 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 e. A /\ x e. A)) -> ((H` v) = (H` x) <-> x = v))
6	5	anassrs 338	. . . . . . . . . . . . . . . . . . 19 |- (((H:A-1-1->B /\ v e. A) /\ x e. A) -> ((H` v) = (H` x) <-> x = v))
7	6	anbi1d 469	. . . . . . . . . . . . . . . . . 18 |- (((H:A-1-1->B /\ v e. A) /\ x e. 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 e. A) /\ x e. 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 e. A) /\ x e. A) -> (E.y e. A (((H` v) = (H` x) /\ (H` u) = (H` y)) /\ xRy) <-> E.y e. A (x = v /\ ((H` u) = (H` y) /\ xRy))))
11		r19.42v 1303	. . . . . . . . . . . . . . . 16 |- (E.y e. A (x = v /\ ((H` u) = (H` y) /\ xRy)) <-> (x = v /\ E.y e. A ((H` u) = (H` y) /\ xRy)))
12	10, 11	syl6bb 414	. . . . . . . . . . . . . . 15 |- (((H:A-1-1->B /\ v e. A) /\ x e. A) -> (E.y e. A (((H` v) = (H` x) /\ (H` u) = (H` y)) /\ xRy) <-> (x = v /\ E.y e. A ((H` u) = (H` y) /\ xRy))))
13	12	birexdva 1216	. . . . . . . . . . . . . 14 |- ((H:A-1-1->B /\ v e. A) -> (E.x e. A E.y e. A (((H` v) = (H` x) /\ (H` u) = (H` y)) /\ xRy) <-> E.x e. A (x = v /\ E.y e. 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 -> (E.y e. A ((H` u) = (H` y) /\ xRy) <-> E.y e. A ((H` u) = (H` y) /\ vRy)))
17	16	ceqsrexv 1413	. . . . . . . . . . . . . . 15 |- (v e. A -> (E.x e. A (x = v /\ E.y e. A ((H` u) = (H` y) /\ xRy)) <-> E.y e. A ((H` u) = (H` y) /\ vRy)))
18	17	adantl 305	. . . . . . . . . . . . . 14 |- ((H:A-1-1->B /\ v e. A) -> (E.x e. A (x = v /\ E.y e. A ((H` u) = (H` y) /\ xRy)) <-> E.y e. A ((H` u) = (H` y) /\ vRy)))
19	13, 18	bitrd 406	. . . . . . . . . . . . 13 |- ((H:A-1-1->B /\ v e. A) -> (E.x e. A E.y e. A (((H` v) = (H` x) /\ (H` u) = (H` y)) /\ xRy) <-> E.y e. A ((H` u) = (H` y) /\ vRy)))
20		f1fveq 2918	. . . . . . . . . . . . . . . . . 18 |- ((H:A-1-1->B /\ (u e. A /\ y e. 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 e. A /\ y e. A)) -> ((H` u) = (H` y) <-> y = u))
23	22	anassrs 338	. . . . . . . . . . . . . . . 16 |- (((H:A-1-1->B /\ u e. A) /\ y e. A) -> ((H` u) = (H` y) <-> y = u))
24	23	anbi1d 469	. . . . . . . . . . . . . . 15 |- (((H:A-1-1->B /\ u e. A) /\ y e. A) -> (((H` u) = (H` y) /\ vRy) <-> (y = u /\ vRy)))
25	24	birexdva 1216	. . . . . . . . . . . . . 14 |- ((H:A-1-1->B /\ u e. A) -> (E.y e. A ((H` u) = (H` y) /\ vRy) <-> E.y e. A (y = u /\ vRy)))
26		breq2 2066	. . . . . . . . . . . . . . . 16 |- (y = u -> (vRy <-> vRu))
27	26	ceqsrexv 1413	. . . . . . . . . . . . . . 15 |- (u e. A -> (E.y e. A (y = u /\ vRy) <-> vRu))
28	27	adantl 305	. . . . . . . . . . . . . 14 |- ((H:A-1-1->B /\ u e. A) -> (E.y e. A (y = u /\ vRy) <-> vRu))
29	25, 28	bitrd 406	. . . . . . . . . . . . 13 |- ((H:A-1-1->B /\ u e. A) -> (E.y e. A ((H` u) = (H` y) /\ vRy) <-> vRu))
30	19, 29	sylan9bb 418	. . . . . . . . . . . 12 |- (((H:A-1-1->B /\ v e. A) /\ (H:A-1-1->B /\ u e. A)) -> (E.x e. A E.y e. A (((H` v) = (H` x) /\ (H` u) = (H` y)) /\ xRy) <-> vRu))
31	30	anandis 394	. . . . . . . . . . 11 |- ((H:A-1-1->B /\ (v e. A /\ u e. A)) -> (E.x e. A E.y e. A (((H` v) = (H` x) /\ (H` u) = (H` y)) /\ xRy) <-> vRu))
32		fvex 2838	. . . . . . . . . . . 12 |- (H` v) e. V
33		fvex 2838	. . . . . . . . . . . 12 |- (H` u) e. 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) -> (E.y e. A ((z = (H` x) /\ w = (H` y)) /\ xRy) <-> E.y e. A (((H` v) = (H` x) /\ w = (H` y)) /\ xRy)))
38	37	birexdv 1220	. . . . . . . . . . . 12 |- (z = (H` v) -> (E.x e. A E.y e. A ((z = (H` x) /\ w = (H` y)) /\ xRy) <-> E.x e. A E.y e. 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) = (