dfac12lem2

	Ref	Expression
Hypotheses	dfac12.1	\|- ( ph -> A e. On )
	dfac12.3	\|- ( ph -> F : ~P ( har ` ( R1 ` A ) ) -1-1-> On )
	dfac12.4	\|- G = recs ( ( x e. _V \|-> ( y e. ( R1 ` dom x ) \|-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) ) )
	dfac12.5	\|- ( ph -> C e. On )
	dfac12.h	\|- H = ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) )
	dfac12.6	\|- ( ph -> C C_ A )
	dfac12.8	\|- ( ph -> A. z e. C ( G ` z ) : ( R1 ` z ) -1-1-> On )
Assertion	dfac12lem2	\|- ( ph -> ( G ` C ) : ( R1 ` C ) -1-1-> On )

Proof

Step	Hyp	Ref	Expression
1		dfac12.1	\|- ( ph -> A e. On )
2		dfac12.3	\|- ( ph -> F : ~P ( har ` ( R1 ` A ) ) -1-1-> On )
3		dfac12.4	\|- G = recs ( ( x e. _V \|-> ( y e. ( R1 ` dom x ) \|-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) ) )
4		dfac12.5	\|- ( ph -> C e. On )
5		dfac12.h	\|- H = ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) )
6		dfac12.6	\|- ( ph -> C C_ A )
7		dfac12.8	\|- ( ph -> A. z e. C ( G ` z ) : ( R1 ` z ) -1-1-> On )
8	3	tfr1	\|- G Fn On
9		fnfun	\|- ( G Fn On -> Fun G )
10	8 9	ax-mp	\|- Fun G
11		funimaexg	\|- ( ( Fun G /\ C e. On ) -> ( G " C ) e. _V )
12	10 4 11	sylancr	\|- ( ph -> ( G " C ) e. _V )
13		uniexg	\|- ( ( G " C ) e. _V -> U. ( G " C ) e. _V )
14		rnexg	\|- ( U. ( G " C ) e. _V -> ran U. ( G " C ) e. _V )
15	12 13 14	3syl	\|- ( ph -> ran U. ( G " C ) e. _V )
16		f1f	\|- ( ( G ` z ) : ( R1 ` z ) -1-1-> On -> ( G ` z ) : ( R1 ` z ) --> On )
17		fssxp	\|- ( ( G ` z ) : ( R1 ` z ) --> On -> ( G ` z ) C_ ( ( R1 ` z ) X. On ) )
18		ssv	\|- ( R1 ` z ) C_ _V
19		xpss1	\|- ( ( R1 ` z ) C_ _V -> ( ( R1 ` z ) X. On ) C_ ( _V X. On ) )
20	18 19	ax-mp	\|- ( ( R1 ` z ) X. On ) C_ ( _V X. On )
21		sstr	\|- ( ( ( G ` z ) C_ ( ( R1 ` z ) X. On ) /\ ( ( R1 ` z ) X. On ) C_ ( _V X. On ) ) -> ( G ` z ) C_ ( _V X. On ) )
22	20 21	mpan2	\|- ( ( G ` z ) C_ ( ( R1 ` z ) X. On ) -> ( G ` z ) C_ ( _V X. On ) )
23		fvex	\|- ( G ` z ) e. _V
24	23	elpw	\|- ( ( G ` z ) e. ~P ( _V X. On ) <-> ( G ` z ) C_ ( _V X. On ) )
25	22 24	sylibr	\|- ( ( G ` z ) C_ ( ( R1 ` z ) X. On ) -> ( G ` z ) e. ~P ( _V X. On ) )
26	16 17 25	3syl	\|- ( ( G ` z ) : ( R1 ` z ) -1-1-> On -> ( G ` z ) e. ~P ( _V X. On ) )
27	26	ralimi	\|- ( A. z e. C ( G ` z ) : ( R1 ` z ) -1-1-> On -> A. z e. C ( G ` z ) e. ~P ( _V X. On ) )
28	7 27	syl	\|- ( ph -> A. z e. C ( G ` z ) e. ~P ( _V X. On ) )
29		onss	\|- ( C e. On -> C C_ On )
30	4 29	syl	\|- ( ph -> C C_ On )
31	8	fndmi	\|- dom G = On
32	30 31	sseqtrrdi	\|- ( ph -> C C_ dom G )
33		funimass4	\|- ( ( Fun G /\ C C_ dom G ) -> ( ( G " C ) C_ ~P ( _V X. On ) <-> A. z e. C ( G ` z ) e. ~P ( _V X. On ) ) )
34	10 32 33	sylancr	\|- ( ph -> ( ( G " C ) C_ ~P ( _V X. On ) <-> A. z e. C ( G ` z ) e. ~P ( _V X. On ) ) )
35	28 34	mpbird	\|- ( ph -> ( G " C ) C_ ~P ( _V X. On ) )
36		sspwuni	\|- ( ( G " C ) C_ ~P ( _V X. On ) <-> U. ( G " C ) C_ ( _V X. On ) )
37	35 36	sylib	\|- ( ph -> U. ( G " C ) C_ ( _V X. On ) )
38		rnss	\|- ( U. ( G " C ) C_ ( _V X. On ) -> ran U. ( G " C ) C_ ran ( _V X. On ) )
39	37 38	syl	\|- ( ph -> ran U. ( G " C ) C_ ran ( _V X. On ) )
40		rnxpss	\|- ran ( _V X. On ) C_ On
41	39 40	sstrdi	\|- ( ph -> ran U. ( G " C ) C_ On )
42		ssonuni	\|- ( ran U. ( G " C ) e. _V -> ( ran U. ( G " C ) C_ On -> U. ran U. ( G " C ) e. On ) )
43	15 41 42	sylc	\|- ( ph -> U. ran U. ( G " C ) e. On )
44		onsuc	\|- ( U. ran U. ( G " C ) e. On -> suc U. ran U. ( G " C ) e. On )
45	43 44	syl	\|- ( ph -> suc U. ran U. ( G " C ) e. On )
46	45	ad2antrr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> suc U. ran U. ( G " C ) e. On )
47		rankon	\|- ( rank ` y ) e. On
48		omcl	\|- ( ( suc U. ran U. ( G " C ) e. On /\ ( rank ` y ) e. On ) -> ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) e. On )
49	46 47 48	sylancl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) e. On )
50		fveq2	\|- ( z = suc ( rank ` y ) -> ( G ` z ) = ( G ` suc ( rank ` y ) ) )
51		f1eq1	\|- ( ( G ` z ) = ( G ` suc ( rank ` y ) ) -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` suc ( rank ` y ) ) : ( R1 ` z ) -1-1-> On ) )
52	50 51	syl	\|- ( z = suc ( rank ` y ) -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` suc ( rank ` y ) ) : ( R1 ` z ) -1-1-> On ) )
53		fveq2	\|- ( z = suc ( rank ` y ) -> ( R1 ` z ) = ( R1 ` suc ( rank ` y ) ) )
54		f1eq2	\|- ( ( R1 ` z ) = ( R1 ` suc ( rank ` y ) ) -> ( ( G ` suc ( rank ` y ) ) : ( R1 ` z ) -1-1-> On <-> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On ) )
55	53 54	syl	\|- ( z = suc ( rank ` y ) -> ( ( G ` suc ( rank ` y ) ) : ( R1 ` z ) -1-1-> On <-> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On ) )
56	52 55	bitrd	\|- ( z = suc ( rank ` y ) -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On ) )
57	7	ad2antrr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> A. z e. C ( G ` z ) : ( R1 ` z ) -1-1-> On )
58		rankr1ai	\|- ( y e. ( R1 ` C ) -> ( rank ` y ) e. C )
59	58	ad2antlr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( rank ` y ) e. C )
60		simpr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> C = U. C )
61	59 60	eleqtrd	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( rank ` y ) e. U. C )
62		eloni	\|- ( C e. On -> Ord C )
63	4 62	syl	\|- ( ph -> Ord C )
64	63	ad2antrr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> Ord C )
65		ordsucuniel	\|- ( Ord C -> ( ( rank ` y ) e. U. C <-> suc ( rank ` y ) e. C ) )
66	64 65	syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( rank ` y ) e. U. C <-> suc ( rank ` y ) e. C ) )
67	61 66	mpbid	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> suc ( rank ` y ) e. C )
68	56 57 67	rspcdva	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On )
69		f1f	\|- ( ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On -> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) --> On )
70	68 69	syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) --> On )
71		r1elwf	\|- ( y e. ( R1 ` C ) -> y e. U. ( R1 " On ) )
72	71	ad2antlr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> y e. U. ( R1 " On ) )
73		rankidb	\|- ( y e. U. ( R1 " On ) -> y e. ( R1 ` suc ( rank ` y ) ) )
74	72 73	syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> y e. ( R1 ` suc ( rank ` y ) ) )
75	70 74	ffvelcdmd	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. On )
76		oacl	\|- ( ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) e. On /\ ( ( G ` suc ( rank ` y ) ) ` y ) e. On ) -> ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) e. On )
77	49 75 76	syl2anc	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) e. On )
78		f1f	\|- ( F : ~P ( har ` ( R1 ` A ) ) -1-1-> On -> F : ~P ( har ` ( R1 ` A ) ) --> On )
79	2 78	syl	\|- ( ph -> F : ~P ( har ` ( R1 ` A ) ) --> On )
80	79	ad2antrr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> F : ~P ( har ` ( R1 ` A ) ) --> On )
81		imassrn	\|- ( H " y ) C_ ran H
82		fvex	\|- ( G ` U. C ) e. _V
83	82	rnex	\|- ran ( G ` U. C ) e. _V
84		fveq2	\|- ( z = U. C -> ( G ` z ) = ( G ` U. C ) )
85		f1eq1	\|- ( ( G ` z ) = ( G ` U. C ) -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` U. C ) : ( R1 ` z ) -1-1-> On ) )
86	84 85	syl	\|- ( z = U. C -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` U. C ) : ( R1 ` z ) -1-1-> On ) )
87		fveq2	\|- ( z = U. C -> ( R1 ` z ) = ( R1 ` U. C ) )
88		f1eq2	\|- ( ( R1 ` z ) = ( R1 ` U. C ) -> ( ( G ` U. C ) : ( R1 ` z ) -1-1-> On <-> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On ) )
89	87 88	syl	\|- ( z = U. C -> ( ( G ` U. C ) : ( R1 ` z ) -1-1-> On <-> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On ) )
90	86 89	bitrd	\|- ( z = U. C -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On ) )
91	7	ad2antrr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> A. z e. C ( G ` z ) : ( R1 ` z ) -1-1-> On )
92	4	ad2antrr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> C e. On )
93		onuni	\|- ( C e. On -> U. C e. On )
94		sucidg	\|- ( U. C e. On -> U. C e. suc U. C )
95	92 93 94	3syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> U. C e. suc U. C )
96	63	adantr	\|- ( ( ph /\ y e. ( R1 ` C ) ) -> Ord C )
97		orduniorsuc	\|- ( Ord C -> ( C = U. C \/ C = suc U. C ) )
98	96 97	syl	\|- ( ( ph /\ y e. ( R1 ` C ) ) -> ( C = U. C \/ C = suc U. C ) )
99	98	orcanai	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> C = suc U. C )
100	95 99	eleqtrrd	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> U. C e. C )
101	90 91 100	rspcdva	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On )
102		f1f	\|- ( ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On -> ( G ` U. C ) : ( R1 ` U. C ) --> On )
103		frn	\|- ( ( G ` U. C ) : ( R1 ` U. C ) --> On -> ran ( G ` U. C ) C_ On )
104	101 102 103	3syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran ( G ` U. C ) C_ On )
105		epweon	\|- _E We On
106		wess	\|- ( ran ( G ` U. C ) C_ On -> ( _E We On -> _E We ran ( G ` U. C ) ) )
107	104 105 106	mpisyl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> _E We ran ( G ` U. C ) )
108		eqid	\|- OrdIso ( _E , ran ( G ` U. C ) ) = OrdIso ( _E , ran ( G ` U. C ) )
109	108	oiiso	\|- ( ( ran ( G ` U. C ) e. _V /\ _E We ran ( G ` U. C ) ) -> OrdIso ( _E , ran ( G ` U. C ) ) Isom _E , _E ( dom OrdIso ( _E , ran ( G ` U. C ) ) , ran ( G ` U. C ) ) )
110	83 107 109	sylancr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> OrdIso ( _E , ran ( G ` U. C ) ) Isom _E , _E ( dom OrdIso ( _E , ran ( G ` U. C ) ) , ran ( G ` U. C ) ) )
111		isof1o	\|- ( OrdIso ( _E , ran ( G ` U. C ) ) Isom _E , _E ( dom OrdIso ( _E , ran ( G ` U. C ) ) , ran ( G ` U. C ) ) -> OrdIso ( _E , ran ( G ` U. C ) ) : dom OrdIso ( _E , ran ( G ` U. C ) ) -1-1-onto-> ran ( G ` U. C ) )
112		f1ocnv	\|- ( OrdIso ( _E , ran ( G ` U. C ) ) : dom OrdIso ( _E , ran ( G ` U. C ) ) -1-1-onto-> ran ( G ` U. C ) -> `' OrdIso ( _E , ran ( G ` U. C ) ) : ran ( G ` U. C ) -1-1-onto-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
113		f1of1	\|- ( `' OrdIso ( _E , ran ( G ` U. C ) ) : ran ( G ` U. C ) -1-1-onto-> dom OrdIso ( _E , ran ( G ` U. C ) ) -> `' OrdIso ( _E , ran ( G ` U. C ) ) : ran ( G ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
114	110 111 112 113	4syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> `' OrdIso ( _E , ran ( G ` U. C ) ) : ran ( G ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
115		f1f1orn	\|- ( ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On -> ( G ` U. C ) : ( R1 ` U. C ) -1-1-onto-> ran ( G ` U. C ) )
116		f1of1	\|- ( ( G ` U. C ) : ( R1 ` U. C ) -1-1-onto-> ran ( G ` U. C ) -> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> ran ( G ` U. C ) )
117	101 115 116	3syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> ran ( G ` U. C ) )
118		f1co	\|- ( ( `' OrdIso ( _E , ran ( G ` U. C ) ) : ran ( G ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) /\ ( G ` U. C ) : ( R1 ` U. C ) -1-1-> ran ( G ` U. C ) ) -> ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
119	114 117 118	syl2anc	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
120		f1eq1	\|- ( H = ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) -> ( H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) <-> ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) ) )
121	5 120	ax-mp	\|- ( H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) <-> ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
122	119 121	sylibr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
123		f1f	\|- ( H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) -> H : ( R1 ` U. C ) --> dom OrdIso ( _E , ran ( G ` U. C ) ) )
124		frn	\|- ( H : ( R1 ` U. C ) --> dom OrdIso ( _E , ran ( G ` U. C ) ) -> ran H C_ dom OrdIso ( _E , ran ( G ` U. C ) ) )
125	122 123 124	3syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran H C_ dom OrdIso ( _E , ran ( G ` U. C ) ) )
126		harcl	\|- ( har ` ( R1 ` A ) ) e. On
127	126	onordi	\|- Ord ( har ` ( R1 ` A ) )
128	108	oion	\|- ( ran ( G ` U. C ) e. _V -> dom OrdIso ( _E , ran ( G ` U. C ) ) e. On )
129	83 128	mp1i	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) e. On )
130	108	oien	\|- ( ( ran ( G ` U. C ) e. _V /\ _E We ran ( G ` U. C ) ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) ~~ ran ( G ` U. C ) )
131	83 107 130	sylancr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) ~~ ran ( G ` U. C ) )
132		fvex	\|- ( R1 ` U. C ) e. _V
133	132	f1oen	\|- ( ( G ` U. C ) : ( R1 ` U. C ) -1-1-onto-> ran ( G ` U. C ) -> ( R1 ` U. C ) ~~ ran ( G ` U. C ) )
134		ensym	\|- ( ( R1 ` U. C ) ~~ ran ( G ` U. C ) -> ran ( G ` U. C ) ~~ ( R1 ` U. C ) )
135	101 115 133 134	4syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran ( G ` U. C ) ~~ ( R1 ` U. C ) )
136		fvex	\|- ( R1 ` A ) e. _V
137	1	ad2antrr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> A e. On )
138	6	ad2antrr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> C C_ A )
139	138 100	sseldd	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> U. C e. A )
140		r1ord2	\|- ( A e. On -> ( U. C e. A -> ( R1 ` U. C ) C_ ( R1 ` A ) ) )
141	137 139 140	sylc	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( R1 ` U. C ) C_ ( R1 ` A ) )
142		ssdomg	\|- ( ( R1 ` A ) e. _V -> ( ( R1 ` U. C ) C_ ( R1 ` A ) -> ( R1 ` U. C ) ~<_ ( R1 ` A ) ) )
143	136 141 142	mpsyl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( R1 ` U. C ) ~<_ ( R1 ` A ) )
144		endomtr	\|- ( ( ran ( G ` U. C ) ~~ ( R1 ` U. C ) /\ ( R1 ` U. C ) ~<_ ( R1 ` A ) ) -> ran ( G ` U. C ) ~<_ ( R1 ` A ) )
145	135 143 144	syl2anc	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran ( G ` U. C ) ~<_ ( R1 ` A ) )
146		endomtr	\|- ( ( dom OrdIso ( _E , ran ( G ` U. C ) ) ~~ ran ( G ` U. C ) /\ ran ( G ` U. C ) ~<_ ( R1 ` A ) ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) ~<_ ( R1 ` A ) )
147	131 145 146	syl2anc	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) ~<_ ( R1 ` A ) )
148		elharval	\|- ( dom OrdIso ( _E , ran ( G ` U. C ) ) e. ( har ` ( R1 ` A ) ) <-> ( dom OrdIso ( _E , ran ( G ` U. C ) ) e. On /\ dom OrdIso ( _E , ran ( G ` U. C ) ) ~<_ ( R1 ` A ) ) )
149	129 147 148	sylanbrc	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) e. ( har ` ( R1 ` A ) ) )
150		ordelss	\|- ( ( Ord ( har ` ( R1 ` A ) ) /\ dom OrdIso ( _E , ran ( G ` U. C ) ) e. ( har ` ( R1 ` A ) ) ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) C_ ( har ` ( R1 ` A ) ) )
151	127 149 150	sylancr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) C_ ( har ` ( R1 ` A ) ) )
152	125 151	sstrd	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran H C_ ( har ` ( R1 ` A ) ) )
153	81 152	sstrid	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( H " y ) C_ ( har ` ( R1 ` A ) ) )
154		fvex	\|- ( har ` ( R1 ` A ) ) e. _V
155	154	elpw2	\|- ( ( H " y ) e. ~P ( har ` ( R1 ` A ) ) <-> ( H " y ) C_ ( har ` ( R1 ` A ) ) )
156	153 155	sylibr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( H " y ) e. ~P ( har ` ( R1 ` A ) ) )
157	80 156	ffvelcdmd	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( F ` ( H " y ) ) e. On )
158	77 157	ifclda	\|- ( ( ph /\ y e. ( R1 ` C ) ) -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) e. On )
159	158	ex	\|- ( ph -> ( y e. ( R1 ` C ) -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) e. On ) )
160		iftrue	\|- ( C = U. C -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) )
161		iftrue	\|- ( C = U. C -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) )
162	160 161	eqeq12d	\|- ( C = U. C -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) ) )
163	162	adantl	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) ) )
164	45	ad2antrr	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> suc U. ran U. ( G " C ) e. On )
165		nsuceq0	\|- suc U. ran U. ( G " C ) =/= (/)
166	165	a1i	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> suc U. ran U. ( G " C ) =/= (/) )
167	47	a1i	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( rank ` y ) e. On )
168		onsucuni	\|- ( ran U. ( G " C ) C_ On -> ran U. ( G " C ) C_ suc U. ran U. ( G " C ) )
169	41 168	syl	\|- ( ph -> ran U. ( G " C ) C_ suc U. ran U. ( G " C ) )
170	169	ad2antrr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ran U. ( G " C ) C_ suc U. ran U. ( G " C ) )
171	30	ad2antrr	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> C C_ On )
172		fnfvima	\|- ( ( G Fn On /\ C C_ On /\ suc ( rank ` y ) e. C ) -> ( G ` suc ( rank ` y ) ) e. ( G " C ) )
173	8 171 67 172	mp3an2i	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( G ` suc ( rank ` y ) ) e. ( G " C ) )
174		elssuni	\|- ( ( G ` suc ( rank ` y ) ) e. ( G " C ) -> ( G ` suc ( rank ` y ) ) C_ U. ( G " C ) )
175		rnss	\|- ( ( G ` suc ( rank ` y ) ) C_ U. ( G " C ) -> ran ( G ` suc ( rank ` y ) ) C_ ran U. ( G " C ) )
176	173 174 175	3syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ran ( G ` suc ( rank ` y ) ) C_ ran U. ( G " C ) )
177		f1fn	\|- ( ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On -> ( G ` suc ( rank ` y ) ) Fn ( R1 ` suc ( rank ` y ) ) )
178	68 177	syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( G ` suc ( rank ` y ) ) Fn ( R1 ` suc ( rank ` y ) ) )
179		fnfvelrn	\|- ( ( ( G ` suc ( rank ` y ) ) Fn ( R1 ` suc ( rank ` y ) ) /\ y e. ( R1 ` suc ( rank ` y ) ) ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. ran ( G ` suc ( rank ` y ) ) )
180	178 74 179	syl2anc	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. ran ( G ` suc ( rank ` y ) ) )
181	176 180	sseldd	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. ran U. ( G " C ) )
182	170 181	sseldd	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. suc U. ran U. ( G " C ) )
183	182	adantlrr	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. suc U. ran U. ( G " C ) )
184		rankon	\|- ( rank ` z ) e. On
185	184	a1i	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( rank ` z ) e. On )
186		eleq1w	\|- ( y = z -> ( y e. ( R1 ` C ) <-> z e. ( R1 ` C ) ) )
187	186	anbi2d	\|- ( y = z -> ( ( ph /\ y e. ( R1 ` C ) ) <-> ( ph /\ z e. ( R1 ` C ) ) ) )
188	187	anbi1d	\|- ( y = z -> ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) <-> ( ( ph /\ z e. ( R1 ` C ) ) /\ C = U. C ) ) )
189		fveq2	\|- ( y = z -> ( rank ` y ) = ( rank ` z ) )
190		suceq	\|- ( ( rank ` y ) = ( rank ` z ) -> suc ( rank ` y ) = suc ( rank ` z ) )
191	189 190	syl	\|- ( y = z -> suc ( rank ` y ) = suc ( rank ` z ) )
192	191	fveq2d	\|- ( y = z -> ( G ` suc ( rank ` y ) ) = ( G ` suc ( rank ` z ) ) )
193		id	\|- ( y = z -> y = z )
194	192 193	fveq12d	\|- ( y = z -> ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) )
195	194	eleq1d	\|- ( y = z -> ( ( ( G ` suc ( rank ` y ) ) ` y ) e. suc U. ran U. ( G " C ) <-> ( ( G ` suc ( rank ` z ) ) ` z ) e. suc U. ran U. ( G " C ) ) )
196	188 195	imbi12d	\|- ( y = z -> ( ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. suc U. ran U. ( G " C ) ) <-> ( ( ( ph /\ z e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` z ) ) ` z ) e. suc U. ran U. ( G " C ) ) ) )
197	196 182	chvarvv	\|- ( ( ( ph /\ z e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` z ) ) ` z ) e. suc U. ran U. ( G " C ) )
198	197	adantlrl	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` z ) ) ` z ) e. suc U. ran U. ( G " C ) )
199		omopth2	\|- ( ( ( suc U. ran U. ( G " C ) e. On /\ suc U. ran U. ( G " C ) =/= (/) ) /\ ( ( rank ` y ) e. On /\ ( ( G ` suc ( rank ` y ) ) ` y ) e. suc U. ran U. ( G " C ) ) /\ ( ( rank ` z ) e. On /\ ( ( G ` suc ( rank ` z ) ) ` z ) e. suc U. ran U. ( G " C ) ) ) -> ( ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) <-> ( ( rank ` y ) = ( rank ` z ) /\ ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) ) )
200	164 166 167 183 185 198 199	syl222anc	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) <-> ( ( rank ` y ) = ( rank ` z ) /\ ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) ) )
201	190	adantl	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> suc ( rank ` y ) = suc ( rank ` z ) )
202	201	fveq2d	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( G ` suc ( rank ` y ) ) = ( G ` suc ( rank ` z ) ) )
203	202	fveq1d	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( ( G ` suc ( rank ` y ) ) ` z ) = ( ( G ` suc ( rank ` z ) ) ` z ) )
204	203	eqeq2d	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` y ) ) ` z ) <-> ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) )
205	68	adantlrr	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On )
206	205	adantr	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On )
207	74	adantlrr	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> y e. ( R1 ` suc ( rank ` y ) ) )
208	207	adantr	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> y e. ( R1 ` suc ( rank ` y ) ) )
209		r1elwf	\|- ( z e. ( R1 ` C ) -> z e. U. ( R1 " On ) )
210		rankidb	\|- ( z e. U. ( R1 " On ) -> z e. ( R1 ` suc ( rank ` z ) ) )
211	209 210	syl	\|- ( z e. ( R1 ` C ) -> z e. ( R1 ` suc ( rank ` z ) ) )
212	211	ad2antll	\|- ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) -> z e. ( R1 ` suc ( rank ` z ) ) )
213	212	ad2antrr	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> z e. ( R1 ` suc ( rank ` z ) ) )
214	201	fveq2d	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( R1 ` suc ( rank ` y ) ) = ( R1 ` suc ( rank ` z ) ) )
215	213 214	eleqtrrd	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> z e. ( R1 ` suc ( rank ` y ) ) )
216		f1fveq	\|- ( ( ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On /\ ( y e. ( R1 ` suc ( rank ` y ) ) /\ z e. ( R1 ` suc ( rank ` y ) ) ) ) -> ( ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` y ) ) ` z ) <-> y = z ) )
217	206 208 215 216	syl12anc	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` y ) ) ` z ) <-> y = z ) )
218	204 217	bitr3d	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) <-> y = z ) )
219	218	biimpd	\|- ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) -> y = z ) )
220	219	expimpd	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( ( ( rank ` y ) = ( rank ` z ) /\ ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) -> y = z ) )
221	189 194	jca	\|- ( y = z -> ( ( rank ` y ) = ( rank ` z ) /\ ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) )
222	220 221	impbid1	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( ( ( rank ` y ) = ( rank ` z ) /\ ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) <-> y = z ) )
223	163 200 222	3bitrd	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> y = z ) )
224		iffalse	\|- ( -. C = U. C -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = ( F ` ( H " y ) ) )
225		iffalse	\|- ( -. C = U. C -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) = ( F ` ( H " z ) ) )
226	224 225	eqeq12d	\|- ( -. C = U. C -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> ( F ` ( H " y ) ) = ( F ` ( H " z ) ) ) )
227	226	adantl	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> ( F ` ( H " y ) ) = ( F ` ( H " z ) ) ) )
228	2	ad2antrr	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> F : ~P ( har ` ( R1 ` A ) ) -1-1-> On )
229	156	adantlrr	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( H " y ) e. ~P ( har ` ( R1 ` A ) ) )
230	187	anbi1d	\|- ( y = z -> ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) <-> ( ( ph /\ z e. ( R1 ` C ) ) /\ -. C = U. C ) ) )
231		imaeq2	\|- ( y = z -> ( H " y ) = ( H " z ) )
232	231	eleq1d	\|- ( y = z -> ( ( H " y ) e. ~P ( har ` ( R1 ` A ) ) <-> ( H " z ) e. ~P ( har ` ( R1 ` A ) ) ) )
233	230 232	imbi12d	\|- ( y = z -> ( ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( H " y ) e. ~P ( har ` ( R1 ` A ) ) ) <-> ( ( ( ph /\ z e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( H " z ) e. ~P ( har ` ( R1 ` A ) ) ) ) )
234	233 156	chvarvv	\|- ( ( ( ph /\ z e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( H " z ) e. ~P ( har ` ( R1 ` A ) ) )
235	234	adantlrl	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( H " z ) e. ~P ( har ` ( R1 ` A ) ) )
236		f1fveq	\|- ( ( F : ~P ( har ` ( R1 ` A ) ) -1-1-> On /\ ( ( H " y ) e. ~P ( har ` ( R1 ` A ) ) /\ ( H " z ) e. ~P ( har ` ( R1 ` A ) ) ) ) -> ( ( F ` ( H " y ) ) = ( F ` ( H " z ) ) <-> ( H " y ) = ( H " z ) ) )
237	228 229 235 236	syl12anc	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( ( F ` ( H " y ) ) = ( F ` ( H " z ) ) <-> ( H " y ) = ( H " z ) ) )
238	122	adantlrr	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
239		simplrl	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> y e. ( R1 ` C ) )
240	99	fveq2d	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( R1 ` C ) = ( R1 ` suc U. C ) )
241		r1suc	\|- ( U. C e. On -> ( R1 ` suc U. C ) = ~P ( R1 ` U. C ) )
242	92 93 241	3syl	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( R1 ` suc U. C ) = ~P ( R1 ` U. C ) )
243	240 242	eqtrd	\|- ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( R1 ` C ) = ~P ( R1 ` U. C ) )
244	243	adantlrr	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( R1 ` C ) = ~P ( R1 ` U. C ) )
245	239 244	eleqtrd	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> y e. ~P ( R1 ` U. C ) )
246	245	elpwid	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> y C_ ( R1 ` U. C ) )
247		simplrr	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> z e. ( R1 ` C ) )
248	247 244	eleqtrd	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> z e. ~P ( R1 ` U. C ) )
249	248	elpwid	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> z C_ ( R1 ` U. C ) )
250		f1imaeq	\|- ( ( H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) /\ ( y C_ ( R1 ` U. C ) /\ z C_ ( R1 ` U. C ) ) ) -> ( ( H " y ) = ( H " z ) <-> y = z ) )
251	238 246 249 250	syl12anc	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( ( H " y ) = ( H " z ) <-> y = z ) )
252	227 237 251	3bitrd	\|- ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> y = z ) )
253	223 252	pm2.61dan	\|- ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> y = z ) )
254	253	ex	\|- ( ph -> ( ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> y = z ) ) )
255	159 254	dom2lem	\|- ( ph -> ( y e. ( R1 ` C ) \|-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) : ( R1 ` C ) -1-1-> On )
256	1 2 3 4 5	dfac12lem1	\|- ( ph -> ( G ` C ) = ( y e. ( R1 ` C ) \|-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) )
257		f1eq1	\|- ( ( G ` C ) = ( y e. ( R1 ` C ) \|-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) -> ( ( G ` C ) : ( R1 ` C ) -1-1-> On <-> ( y e. ( R1 ` C ) \|-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) : ( R1 ` C ) -1-1-> On ) )
258	256 257	syl	\|- ( ph -> ( ( G ` C ) : ( R1 ` C ) -1-1-> On <-> ( y e. ( R1 ` C ) \|-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) : ( R1 ` C ) -1-1-> On ) )
259	255 258	mpbird	\|- ( ph -> ( G ` C ) : ( R1 ` C ) -1-1-> On )

Metamath Proof Explorer

Theorem dfac12lem2

Proof