Theorem isowe 2941

Description: An isomorphism preserves well ordering. Proposition 6.32(3) of [TakeutiZaring] p. 33.

Assertion

Ref	Expression
isowe	|- (H Isom R, S (A, B) -> (R We A <-> S We B))

Proof of Theorem isowe

Step	Hyp	Ref	Expression
1		isofr 2940	. . 3 |- (H Isom R, S (A, B) -> (R Fr A <-> S Fr B))
2		isorel 2932	. . . . . . . . . 10 |- ((H Isom R, S (A, B) /\ (x e. A /\ y e. A)) -> (xRy <-> (H` x)S(H` y)))
3		f1fveq 2918	. . . . . . . . . . . 12 |- ((H:A-1-1->B /\ (x e. A /\ y e. A)) -> ((H` x) = (H` y) <-> x = y))
4		isof1o 2931	. . . . . . . . . . . . 13 |- (H Isom R, S (A, B) -> H:A-1-1-onto->B)
5		f1of1 2799	. . . . . . . . . . . . 13 |- (H:A-1-1-onto->B -> H:A-1-1->B)
6	4, 5	syl 12	. . . . . . . . . . . 12 |- (H Isom R, S (A, B) -> H:A-1-1->B)
7	3, 6	sylan 343	. . . . . . . . . . 11 |- ((H Isom R, S (A, B) /\ (x e. A /\ y e. A)) -> ((H` x) = (H` y) <-> x = y))
8	7	bicomd 399	. . . . . . . . . 10 |- ((H Isom R, S (A, B) /\ (x e. A /\ y e. A)) -> (x = y <-> (H` x) = (H` y)))
9		isorel 2932	. . . . . . . . . . 11 |- ((H Isom R, S (A, B) /\ (y e. A /\ x e. A)) -> (yRx <-> (H` y)S(H` x)))
10		ancom 333	. . . . . . . . . . 11 |- ((x e. A /\ y e. A) <-> (y e. A /\ x e. A))
11	9, 10	sylan2b 347	. . . . . . . . . 10 |- ((H Isom R, S (A, B) /\ (x e. A /\ y e. A)) -> (yRx <-> (H` y)S(H` x)))
12	2, 8, 11	bi3ord 635	. . . . . . . . 9 |- ((H Isom R, S (A, B) /\ (x e. A /\ y e. A)) -> ((xRy \/ x = y \/ yRx) <-> ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x))))
13	12	exp32 294	. . . . . . . 8 |- (H Isom R, S (A, B) -> (x e. A -> (y e. A -> ((xRy \/ x = y \/ yRx) <-> ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x))))))
14	13	r19.21adv 1262	. . . . . . 7 |- (H Isom R, S (A, B) -> (x e. A -> A.y e. A ((xRy \/ x = y \/ yRx) <-> ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x)))))
15		r19.15 1292	. . . . . . 7 |- (A.y e. A ((xRy \/ x = y \/ yRx) <-> ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x))) -> (A.y e. A (xRy \/ x = y \/ yRx) <-> A.y e. A ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x))))
16	14, 15	syl6 23	. . . . . 6 |- (H Isom R, S (A, B) -> (x e. A -> (A.y e. A (xRy \/ x = y \/ yRx) <-> A.y e. A ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x)))))
17	16	r19.21aiv 1259	. . . . 5 |- (H Isom R, S (A, B) -> A.x e. A (A.y e. A (xRy \/ x = y \/ yRx) <-> A.y e. A ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x))))
18		r19.15 1292	. . . . 5 |- (A.x e. A (A.y e. A (xRy \/ x = y \/ yRx) <-> A.y e. A ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x))) -> (A.x e. A A.y e. A (xRy \/ x = y \/ yRx) <-> A.x e. A A.y e. A ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x))))
19	17, 18	syl 12	. . . 4 |- (H Isom R, S (A, B) -> (A.x e. A A.y e. A (xRy \/ x = y \/ yRx) <-> A.x e. A A.y e. A ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x))))
20		f1ofo 2806	. . . . 5 |- (H:A-1-1-onto->B -> H:A-onto->B)
21		breq2 2066	. . . . . . . . 9 |- ((H` y) = w -> ((H` x)S(H` y) <-> (H` x)Sw))
22		cleq2 1110	. . . . . . . . 9 |- ((H` y) = w -> ((H` x) = (H` y) <-> (H` x) = w))
23		breq1 2065	. . . . . . . . 9 |- ((H` y) = w -> ((H` y)S(H` x) <-> wS(H` x)))
24	21, 22, 23	bi3ord 635	. . . . . . . 8 |- ((H` y) = w -> (((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x)) <-> ((H` x)Sw \/ (H` x) = w \/ wS(H` x))))
25	24	cbvfo 2923	. . . . . . 7 |- (H:A-onto->B -> (A.y e. A ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x)) <-> A.w e. B ((H` x)Sw \/ (H` x) = w \/ wS(H` x))))
26	25	biraldv 1219	. . . . . 6 |- (H:A-onto->B -> (A.x e. A A.y e. A ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x)) <-> A.x e. A A.w e. B ((H` x)Sw \/ (H` x) = w \/ wS(H` x))))
27		breq1 2065	. . . . . . . . 9 |- ((H` x) = z -> ((H` x)Sw <-> zSw))
28		cleq1 1107	. . . . . . . . 9 |- ((H` x) = z -> ((H` x) = w <-> z = w))
29		breq2 2066	. . . . . . . . 9 |- ((H` x) = z -> (wS(H` x) <-> wSz))
30	27, 28, 29	bi3ord 635	. . . . . . . 8 |- ((H` x) = z -> (((H` x)Sw \/ (H` x) = w \/ wS(H` x)) <-> (zSw \/ z = w \/ wSz)))
31	30	biraldv 1219	. . . . . . 7 |- ((H` x) = z -> (A.w e. B ((H` x)Sw \/ (H` x) = w \/ wS(H` x)) <-> A.w e. B (zSw \/ z = w \/ wSz)))
32	31	cbvfo 2923	. . . . . 6 |- (H:A-onto->B -> (A.x e. A A.w e. B ((H` x)Sw \/ (H` x) = w \/ wS(H` x)) <-> A.z e. B A.w e. B (zSw \/ z = w \/ wSz)))
33	26, 32	bitrd 406	. . . . 5 |- (H:A-onto->B -> (A.x e. A A.y e. A ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x)) <-> A.z e. B A.w e. B (zSw \/ z = w \/ wSz)))
34	4, 20, 33	3syl 21	. . . 4 |- (H Isom R, S (A, B) -> (A.x e. A A.y e. A ((H` x)S(H` y) \/ (H` x) = (H` y) \/ (H` y)S(H` x)) <-> A.z e. B A.w e. B (zSw \/ z = w \/ wSz)))
35	19, 34	bitrd 406	. . 3 |- (H Isom R, S (A, B) -> (A.x e. A A.y e. A (xRy \/ x = y \/ yRx) <-> A.z e. B A.w e. B (zSw \/ z = w \/ wSz)))
36	1, 35	anbi12d 476	. 2 |- (H Isom R, S (A, B) -> ((R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)) <-> (S Fr B /\ A.z e. B A.w e. B (zSw \/ z = w \/ wSz))))
37		dfwe2 2187	. 2 |- (R We A <-> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
38		dfwe2 2187	. 2 |- (S We B <-> (S Fr B /\ A.z e. B A.w e. B (zSw \/ z = w \/ wSz)))
39	36, 37, 38	3bitr4g 428	1 |- (H Isom R, S (A, B) -> (R We A <-> S We B))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196   \/ w3o 580   = weq 797   = wceq 1091   e. wcel 1092  A.wral 1201   class class class wbr 2054   Fr wfr 2061   We wwe 2062  -1-1->wf1 2419  -onto->wfo 2420  -1-1-onto->wf1o 2421  ` cfv&nbs