Theorem ordiso2 8420

Description: Generalize ordiso 8421 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.)

Assertion

Ref	Expression
ordiso2	|- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A = B )

Proof of Theorem ordiso2

Dummy variables w x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ordsson 6989	. . . . . 6 |- ( Ord A -> A C_ On )
2	1	3ad2ant2 1083	. . . . 5 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A C_ On )
3	2	sseld 3602	. . . 4 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> x e. On ) )
4		eleq1 2689	. . . . . . . 8 |- ( x = y -> ( x e. A <-> y e. A ) )
5		fveq2 6191	. . . . . . . . 9 |- ( x = y -> ( F ` x ) = ( F ` y ) )
6		id 22	. . . . . . . . 9 |- ( x = y -> x = y )
7	5, 6	eqeq12d 2637	. . . . . . . 8 |- ( x = y -> ( ( F ` x ) = x <-> ( F ` y ) = y ) )
8	4, 7	imbi12d 334	. . . . . . 7 |- ( x = y -> ( ( x e. A -> ( F ` x ) = x ) <-> ( y e. A -> ( F ` y ) = y ) ) )
9	8	imbi2d 330	. . . . . 6 |- ( x = y -> ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( F ` x ) = x ) ) <-> ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( y e. A -> ( F ` y ) = y ) ) ) )
10		r19.21v 2960	. . . . . . 7 |- ( A. y e. x ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( y e. A -> ( F ` y ) = y ) ) <-> ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A. y e. x ( y e. A -> ( F ` y ) = y ) ) )
11		ordelss 5739	. . . . . . . . . . . . . . . 16 |- ( ( Ord A /\ x e. A ) -> x C_ A )
12	11	3ad2antl2 1224	. . . . . . . . . . . . . . 15 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ x e. A ) -> x C_ A )
13	12	sselda 3603	. . . . . . . . . . . . . 14 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ x e. A ) /\ y e. x ) -> y e. A )
14		pm5.5 351	. . . . . . . . . . . . . 14 |- ( y e. A -> ( ( y e. A -> ( F ` y ) = y ) <-> ( F ` y ) = y ) )
15	13, 14	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ x e. A ) /\ y e. x ) -> ( ( y e. A -> ( F ` y ) = y ) <-> ( F ` y ) = y ) )
16	15	ralbidva 2985	. . . . . . . . . . . 12 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ x e. A ) -> ( A. y e. x ( y e. A -> ( F ` y ) = y ) <-> A. y e. x ( F ` y ) = y ) )
17		isof1o 6573	. . . . . . . . . . . . . . . . . . . 20 |- ( F Isom _E , _E ( A , B ) -> F : A -1-1-onto-> B )
18	17	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . 19 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> F : A -1-1-onto-> B )
19	18	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> F : A -1-1-onto-> B )
20		simpll3 1102	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> Ord B )
21		simpr 477	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> z e. ( F ` x ) )
22		f1of 6137	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( F : A -1-1-onto-> B -> F : A --> B )
23	17, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F Isom _E , _E ( A , B ) -> F : A --> B )
24	23	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> F : A --> B )
25	24	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> F : A --> B )
26		simplrl 800	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> x e. A )
27		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
28	25, 26, 27	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> ( F ` x ) e. B )
29	21, 28	jca 554	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> ( z e. ( F ` x ) /\ ( F ` x ) e. B ) )
30		ordtr1 5767	. . . . . . . . . . . . . . . . . . 19 |- ( Ord B -> ( ( z e. ( F ` x ) /\ ( F ` x ) e. B ) -> z e. B ) )
31	20, 29, 30	sylc 65	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> z e. B )
32		f1ocnvfv2 6533	. . . . . . . . . . . . . . . . . 18 |- ( ( F : A -1-1-onto-> B /\ z e. B ) -> ( F ` ( `' F ` z ) ) = z )
33	19, 31, 32	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> ( F ` ( `' F ` z ) ) = z )
34	33, 21	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> ( F ` ( `' F ` z ) ) e. ( F ` x ) )
35		simpll1 1100	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> F Isom _E , _E ( A , B ) )
36		f1ocnv 6149	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )
37		f1of 6137	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( `' F : B -1-1-onto-> A -> `' F : B --> A )
38	19, 36, 37	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> `' F : B --> A )
39		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( `' F : B --> A /\ z e. B ) -> ( `' F ` z ) e. A )
40	38, 31, 39	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> ( `' F ` z ) e. A )
41		isorel 6576	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F Isom _E , _E ( A , B ) /\ ( ( `' F ` z ) e. A /\ x e. A ) ) -> ( ( `' F ` z ) _E x <-> ( F ` ( `' F ` z ) ) _E ( F ` x ) ) )
42	35, 40, 26, 41	syl12anc 1324	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> ( ( `' F ` z ) _E x <-> ( F ` ( `' F ` z ) ) _E ( F ` x ) ) )
43		vex 3203	. . . . . . . . . . . . . . . . . . . . 21 |- x e. _V
44	43	epelc 5031	. . . . . . . . . . . . . . . . . . . 20 |- ( ( `' F ` z ) _E x <-> ( `' F ` z ) e. x )
45		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21 |- ( F ` x ) e. _V
46	45	epelc 5031	. . . . . . . . . . . . . . . . . . . 20 |- ( ( F ` ( `' F ` z ) ) _E ( F ` x ) <-> ( F ` ( `' F ` z ) ) e. ( F ` x ) )
47	42, 44, 46	3bitr3g 302	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> ( ( `' F ` z ) e. x <-> ( F ` ( `' F ` z ) ) e. ( F ` x ) ) )
48	34, 47	mpbird 247	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> ( `' F ` z ) e. x )
49		simplrr 801	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> A. y e. x ( F ` y ) = y )
50		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( y = ( `' F ` z ) -> ( F ` y ) = ( F ` ( `' F ` z ) ) )
51		id 22	. . . . . . . . . . . . . . . . . . . 20 |- ( y = ( `' F ` z ) -> y = ( `' F ` z ) )
52	50, 51	eqeq12d 2637	. . . . . . . . . . . . . . . . . . 19 |- ( y = ( `' F ` z ) -> ( ( F ` y ) = y <-> ( F ` ( `' F ` z ) ) = ( `' F ` z ) ) )
53	52	rspcv 3305	. . . . . . . . . . . . . . . . . 18 |- ( ( `' F ` z ) e. x -> ( A. y e. x ( F ` y ) = y -> ( F ` ( `' F ` z ) ) = ( `' F ` z ) ) )
54	48, 49, 53	sylc 65	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> ( F ` ( `' F ` z ) ) = ( `' F ` z ) )
55	33, 54	eqtr3d 2658	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> z = ( `' F ` z ) )
56	55, 48	eqeltrd 2701	. . . . . . . . . . . . . . 15 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. ( F ` x ) ) -> z e. x )
57		simprr 796	. . . . . . . . . . . . . . . . 17 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) -> A. y e. x ( F ` y ) = y )
58		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> ( F ` y ) = ( F ` z ) )
59		id 22	. . . . . . . . . . . . . . . . . . 19 |- ( y = z -> y = z )
60	58, 59	eqeq12d 2637	. . . . . . . . . . . . . . . . . 18 |- ( y = z -> ( ( F ` y ) = y <-> ( F ` z ) = z ) )
61	60	rspccva 3308	. . . . . . . . . . . . . . . . 17 |- ( ( A. y e. x ( F ` y ) = y /\ z e. x ) -> ( F ` z ) = z )
62	57, 61	sylan 488	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. x ) -> ( F ` z ) = z )
63		epel 5032	. . . . . . . . . . . . . . . . . . . 20 |- ( z _E x <-> z e. x )
64	63	biimpri 218	. . . . . . . . . . . . . . . . . . 19 |- ( z e. x -> z _E x )
65	64	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. x ) -> z _E x )
66		simpll1 1100	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. x ) -> F Isom _E , _E ( A , B ) )
67		simpl2 1065	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) -> Ord A )
68		simprl 794	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) -> x e. A )
69	67, 68, 11	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) -> x C_ A )
70	69	sselda 3603	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. x ) -> z e. A )
71		simplrl 800	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. x ) -> x e. A )
72		isorel 6576	. . . . . . . . . . . . . . . . . . 19 |- ( ( F Isom _E , _E ( A , B ) /\ ( z e. A /\ x e. A ) ) -> ( z _E x <-> ( F ` z ) _E ( F ` x ) ) )
73	66, 70, 71, 72	syl12anc 1324	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. x ) -> ( z _E x <-> ( F ` z ) _E ( F ` x ) ) )
74	65, 73	mpbid 222	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. x ) -> ( F ` z ) _E ( F ` x ) )
75	45	epelc 5031	. . . . . . . . . . . . . . . . 17 |- ( ( F ` z ) _E ( F ` x ) <-> ( F ` z ) e. ( F ` x ) )
76	74, 75	sylib 208	. . . . . . . . . . . . . . . 16 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. x ) -> ( F ` z ) e. ( F ` x ) )
77	62, 76	eqeltrrd 2702	. . . . . . . . . . . . . . 15 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. x ) -> z e. ( F ` x ) )
78	56, 77	impbida 877	. . . . . . . . . . . . . 14 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) -> ( z e. ( F ` x ) <-> z e. x ) )
79	78	eqrdv 2620	. . . . . . . . . . . . 13 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) -> ( F ` x ) = x )
80	79	expr 643	. . . . . . . . . . . 12 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ x e. A ) -> ( A. y e. x ( F ` y ) = y -> ( F ` x ) = x ) )
81	16, 80	sylbid 230	. . . . . . . . . . 11 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ x e. A ) -> ( A. y e. x ( y e. A -> ( F ` y ) = y ) -> ( F ` x ) = x ) )
82	81	ex 450	. . . . . . . . . 10 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( A. y e. x ( y e. A -> ( F ` y ) = y ) -> ( F ` x ) = x ) ) )
83	82	com23 86	. . . . . . . . 9 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( A. y e. x ( y e. A -> ( F ` y ) = y ) -> ( x e. A -> ( F ` x ) = x ) ) )
84	83	a2i 14	. . . . . . . 8 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A. y e. x ( y e. A -> ( F ` y ) = y ) ) -> ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( F ` x ) = x ) ) )
85	84	a1i 11	. . . . . . 7 |- ( x e. On -> ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A. y e. x ( y e. A -> ( F ` y ) = y ) ) -> ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( F ` x ) = x ) ) ) )
86	10, 85	syl5bi 232	. . . . . 6 |- ( x e. On -> ( A. y e. x ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( y e. A -> ( F ` y ) = y ) ) -> ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( F ` x ) = x ) ) ) )
87	9, 86	tfis2 7056	. . . . 5 |- ( x e. On -> ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( F ` x ) = x ) ) )
88	87	com3l 89	. . . 4 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( x e. On -> ( F ` x ) = x ) ) )
89	3, 88	mpdd 43	. . 3 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( F ` x ) = x ) )
90	89	ralrimiv 2965	. 2 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A. x e. A ( F ` x ) = x )
91		fveq2 6191	. . . . . . . . 9 |- ( x = z -> ( F ` x ) = ( F ` z ) )
92		id 22	. . . . . . . . 9 |- ( x = z -> x = z )
93	91, 92	eqeq12d 2637	. . . . . . . 8 |- ( x = z -> ( ( F ` x ) = x <-> ( F ` z ) = z ) )
94	93	rspccva 3308	. . . . . . 7 |- ( ( A. x e. A ( F ` x ) = x /\ z e. A ) -> ( F ` z ) = z )
95	94	adantll 750	. . . . . 6 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) /\ z e. A ) -> ( F ` z ) = z )
96		ffvelrn 6357	. . . . . . . . 9 |- ( ( F : A --> B /\ z e. A ) -> ( F ` z ) e. B )
97	23, 96	sylan 488	. . . . . . . 8 |- ( ( F Isom _E , _E ( A , B ) /\ z e. A ) -> ( F ` z ) e. B )
98	97	3ad2antl1 1223	. . . . . . 7 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ z e. A ) -> ( F ` z ) e. B )
99	98	adantlr 751	. . . . . 6 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) /\ z e. A ) -> ( F ` z ) e. B )
100	95, 99	eqeltrrd 2702	. . . . 5 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) /\ z e. A ) -> z e. B )
101	100	ex 450	. . . 4 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( z e. A -> z e. B ) )
102		simpl1 1064	. . . . . . . 8 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> F Isom _E , _E ( A , B ) )
103		f1ofo 6144	. . . . . . . . 9 |- ( F : A -1-1-onto-> B -> F : A -onto-> B )
104		forn 6118	. . . . . . . . 9 |- ( F : A -onto-> B -> ran F = B )
105	17, 103, 104	3syl 18	. . . . . . . 8 |- ( F Isom _E , _E ( A , B ) -> ran F = B )
106	102, 105	syl 17	. . . . . . 7 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ran F = B )
107	106	eleq2d 2687	. . . . . 6 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( z e. ran F <-> z e. B ) )
108		f1ofn 6138	. . . . . . . . . 10 |- ( F : A -1-1-onto-> B -> F Fn A )
109	17, 108	syl 17	. . . . . . . . 9 |- ( F Isom _E , _E ( A , B ) -> F Fn A )
110	109	3ad2ant1 1082	. . . . . . . 8 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> F Fn A )
111	110	adantr 481	. . . . . . 7 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> F Fn A )
112		fvelrnb 6243	. . . . . . 7 |- ( F Fn A -> ( z e. ran F <-> E. w e. A ( F ` w ) = z ) )
113	111, 112	syl 17	. . . . . 6 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( z e. ran F <-> E. w e. A ( F ` w ) = z ) )
114	107, 113	bitr3d 270	. . . . 5 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( z e. B <-> E. w e. A ( F ` w ) = z ) )
115		fveq2 6191	. . . . . . . . . . . 12 |- ( x = w -> ( F ` x ) = ( F ` w ) )
116		id 22	. . . . . . . . . . . 12 |- ( x = w -> x = w )
117	115, 116	eqeq12d 2637	. . . . . . . . . . 11 |- ( x = w -> ( ( F ` x ) = x <-> ( F ` w ) = w ) )
118	117	rspcv 3305	. . . . . . . . . 10 |- ( w e. A -> ( A. x e. A ( F ` x ) = x -> ( F ` w ) = w ) )
119	118	a1i 11	. . . . . . . . 9 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( w e. A -> ( A. x e. A ( F ` x ) = x -> ( F ` w ) = w ) ) )
120		simpr 477	. . . . . . . . . . . . 13 |- ( ( ( F ` w ) = w /\ ( F ` w ) = z ) -> ( F ` w ) = z )
121		simpl 473	. . . . . . . . . . . . 13 |- ( ( ( F ` w ) = w /\ ( F ` w ) = z ) -> ( F ` w ) = w )
122	120, 121	eqtr3d 2658	. . . . . . . . . . . 12 |- ( ( ( F ` w ) = w /\ ( F ` w ) = z ) -> z = w )
123	122	adantl 482	. . . . . . . . . . 11 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ w e. A ) /\ ( ( F ` w ) = w /\ ( F ` w ) = z ) ) -> z = w )
124		simplr 792	. . . . . . . . . . 11 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ w e. A ) /\ ( ( F ` w ) = w /\ ( F ` w ) = z ) ) -> w e. A )
125	123, 124	eqeltrd 2701	. . . . . . . . . 10 |- ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ w e. A ) /\ ( ( F ` w ) = w /\ ( F ` w ) = z ) ) -> z e. A )
126	125	exp43 640	. . . . . . . . 9 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( w e. A -> ( ( F ` w ) = w -> ( ( F ` w ) = z -> z e. A ) ) ) )
127	119, 126	syldd 72	. . . . . . . 8 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( w e. A -> ( A. x e. A ( F ` x ) = x -> ( ( F ` w ) = z -> z e. A ) ) ) )
128	127	com23 86	. . . . . . 7 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( A. x e. A ( F ` x ) = x -> ( w e. A -> ( ( F ` w ) = z -> z e. A ) ) ) )
129	128	imp 445	. . . . . 6 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( w e. A -> ( ( F ` w ) = z -> z e. A ) ) )
130	129	rexlimdv 3030	. . . . 5 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( E. w e. A ( F ` w ) = z -> z e. A ) )
131	114, 130	sylbid 230	. . . 4 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( z e. B -> z e. A ) )
132	101, 131	impbid 202	. . 3 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( z e. A <-> z e. B ) )
133	132	eqrdv 2620	. 2 |- ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> A = B )
134	90, 133	mpdan 702	1 |- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A = B )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   C_ wss 3574   class class class wbr 4653   _E cep 5028   `'ccnv 5113   ran crn 5115   Ord word 5722   Oncon0 5723   Fn wfn 5883   -->wf 5884   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888   Isom wiso 5889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-ord 5726  df-on 5727  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897

This theorem is referenced by:  ordiso  8421  oieu  8444  oiid  8446