Theorem f1oiso 3895

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 groups:   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 319	. . 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 1532	. . . . . . . . . 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 3867	. . . . . . . . . . . . . . . . . . . . 21 |- ((H:A-1-1->B /\ (v e. A /\ x e. A)) -> ((H` v) = (H` x) <-> v = x))
4		eqcom 1474	. . . . . . . . . . . . . . . . . . . . 21 |- (v = x <-> x = v)
5	3, 4	syl6bb 535	. . . . . . . . . . . . . . . . . . . 20 |- ((H:A-1-1->B /\ (v e. A /\ x e. A)) -> ((H` v) = (H` x) <-> x = v))
6	5	anassrs 441	. . . . . . . . . . . . . . . . . . 19 |- (((H:A-1-1->B /\ v e. A) /\ x e. A) -> ((H` v) = (H` x) <-> x = v))
7	6	anbi1d 616	. . . . . . . . . . . . . . . . . 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 439	. . . . . . . . . . . . . . . . . 18 |- ((((H` v) = (H` x) /\ (H` u) = (H` y)) /\ xRy) <-> ((H` v) = (H` x) /\ ((H` u) = (H` y) /\ xRy)))
9	7, 8	syl5bb 531	. . . . . . . . . . . . . . . . 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	rexbidv 1661	. . . . . . . . . . . . . . . 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 1761	. . . . . . . . . . . . . . . 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 535	. . . . . . . . . . . . . . 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	rexbidva 1657	. . . . . . . . . . . . . 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 2617	. . . . . . . . . . . . . . . . . 18 |- (x = v -> (xRy <-> vRy))
15	14	anbi2d 615	. . . . . . . . . . . . . . . . 17 |- (x = v -> (((H` u) = (H` y) /\ xRy) <-> ((H` u) = (H` y) /\ vRy)))
16	15	rexbidv 1661	. . . . . . . . . . . . . . . 16 |- (x = v -> (E.y e. A ((H` u) = (H` y) /\ xRy) <-> E.y e. A ((H` u) = (H` y) /\ vRy)))
17	16	ceqsrexv 1885	. . . . . . . . . . . . . . 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 388	. . . . . . . . . . . . . 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 527	. . . . . . . . . . . . 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 3867	. . . . . . . . . . . . . . . . . 18 |- ((H:A-1-1->B /\ (u e. A /\ y e. A)) -> ((H` u) = (H` y) <-> u = y))
21		eqcom 1474	. . . . . . . . . . . . . . . . . 18 |- (u = y <-> y = u)
22	20, 21	syl6bb 535	. . . . . . . . . . . . . . . . 17 |- ((H:A-1-1->B /\ (u e. A /\ y e. A)) -> ((H` u) = (H` y) <-> y = u))
23	22	anassrs 441	. . . . . . . . . . . . . . . 16 |- (((H:A-1-1->B /\ u e. A) /\ y e. A) -> ((H` u) = (H` y) <-> y = u))
24	23	anbi1d 616	. . . . . . . . . . . . . . 15 |- (((H:A-1-1->B /\ u e. A) /\ y e. A) -> (((H` u) = (H` y) /\ vRy) <-> (y = u /\ vRy)))
25	24	rexbidva 1657	. . . . . . . . . . . . . 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 2618	. . . . . . . . . . . . . . . 16 |- (y = u -> (vRy <-> vRu))
27	26	ceqsrexv 1885	. . . . . . . . . . . . . . 15 |- (u e. A -> (E.y e. A (y = u /\ vRy) <-> vRu))
28	27	adantl 388	. . . . . . . . . . . . . 14 |- ((H:A-1-1->B /\ u e. A) -> (E.y e. A (y = u /\ vRy) <-> vRu))
29	25, 28	bitrd 527	. . . . . . . . . . . . 13 |- ((H:A-1-1->B /\ u e. A) -> (E.y e. A ((H` u) = (H` y) /\ vRy) <-> vRu))
30	19, 29	sylan9bb 539	. . . . . . . . . . . 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 512	. . . . . . . . . . 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 3723	. . . . . . . . . . . 12 |- (H` v) e. V
33		fvex 3723	. . . . . . . . . . . 12 |- (H` u) e. V
34		eqeq1 1478	. . . . . . . . . . . . . . 15 |- (z = (H` v) -> (z = (H` x) <-> (H` v) = (H` x)))
35	34	anbi1d 616	. . . . . . . . . . . . . 14 |- (z = (H` v) -> ((z = (H` x) /\ w = (H` y)) <-> ((H` v) = (H` x) /\ w = (H` y))))
36	35	anbi1d 616	. . . . . . . . . . . . 13 |- (z = (H` v) -> (((z = (H` x) /\ w = (H` y)) /\ xRy) <-> (((H` v) = (H` x) /\ w = (H` y)) /\ xRy)))
37	36	2rexbidv 1678	. . . . . . . . . . . 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)))
38		eqeq1 1478	. . . . . . . . . . . . . . 15 |- (w = (H` u) -> (w = (H` y) <-> (H` u) = (H` y)))
39	38	anbi2d 615	. . . . . . . . . . . . . 14 |- (w = (H` u) -> (((H` v) = (H` x) /\ w = (H` y)) <-> ((H` v) = (H` x) /\ (H` u) = (H` y))))
40	39	anbi1d 616	. . . . . . . . . . . . 13 |- (w = (H` u) -> ((((H