Theorem cantnflem1 7601

Description: Lemma for cantnf 7605. This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation T is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct F , G are T -related as F < G or G < F, and WLOG assuming that F < G, we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015.)

Hypotheses

Ref	Expression
cantnfs.1	|- S = dom ( A CNF B )
cantnfs.2	|- ( ph -> A e. On )
cantnfs.3	|- ( ph -> B e. On )
oemapval.t	|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
oemapval.3	|- ( ph -> F e. S )
oemapval.4	|- ( ph -> G e. S )
oemapvali.5	|- ( ph -> F T G )
oemapvali.6	|- X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
cantnflem1.o	|- O = OrdIso ( _E , ( `' G " ( _V \ 1o ) ) )
cantnflem1.h	|- H = seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( G ` ( O ` k ) ) ) +o z ) ) , (/) )

Assertion

Ref	Expression
cantnflem1	|- ( ph -> ( ( A CNF B ) ` F ) e. ( ( A CNF B ) ` G ) )

Distinct variable groups:   k, c, w, x, y, z, B   A, c, k, w, x, y, z   T, c, k   k, F, w, x, y, z   S, c, k, x, y, z   G, c, k, w, x, y, z   x, H, y   k, O, w, x, y, z   ph, k, x, y, z   k, X, w, x, y, z   F, c   ph, c

Allowed substitution hints:   ph( w)   S( w)   T( x, y, z, w)   H( z, w, k, c)   O( c)   X( c)

Proof of Theorem cantnflem1

Dummy variable u is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oemapval.3	. . . . . . . 8 |- ( ph -> F e. S )
2		cantnfs.1	. . . . . . . . 9 |- S = dom ( A CNF B )
3		cantnfs.2	. . . . . . . . 9 |- ( ph -> A e. On )
4		cantnfs.3	. . . . . . . . 9 |- ( ph -> B e. On )
5	2, 3, 4	cantnfs 7577	. . . . . . . 8 |- ( ph -> ( F e. S <-> ( F : B --> A /\ ( `' F " ( _V \ 1o ) ) e. Fin ) ) )
6	1, 5	mpbid 202	. . . . . . 7 |- ( ph -> ( F : B --> A /\ ( `' F " ( _V \ 1o ) ) e. Fin ) )
7	6	simpld 446	. . . . . 6 |- ( ph -> F : B --> A )
8	7	feqmptd 5738	. . . . 5 |- ( ph -> F = ( x e. B |-> ( F ` x ) ) )
9		eqeq2 2413	. . . . . . 7 |- ( ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) -> ( ( F ` x ) = ( F ` x ) <-> ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) )
10		eqeq2 2413	. . . . . . 7 |- ( (/) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) -> ( ( F ` x ) = (/) <-> ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) )
11		eqidd 2405	. . . . . . 7 |- ( ( ( ph /\ x e. B ) /\ x C_ ( O ` U. dom O ) ) -> ( F ` x ) = ( F ` x ) )
12		onss 4730	. . . . . . . . . . . . 13 |- ( B e. On -> B C_ On )
13	4, 12	syl 16	. . . . . . . . . . . 12 |- ( ph -> B C_ On )
14	13	sselda 3308	. . . . . . . . . . 11 |- ( ( ph /\ x e. B ) -> x e. On )
15		cnvimass 5183	. . . . . . . . . . . . . . 15 |- ( `' G " ( _V \ 1o ) ) C_ dom G
16		oemapval.4	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G e. S )
17	2, 3, 4	cantnfs 7577	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( G e. S <-> ( G : B --> A /\ ( `' G " ( _V \ 1o ) ) e. Fin ) ) )
18	16, 17	mpbid 202	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G : B --> A /\ ( `' G " ( _V \ 1o ) ) e. Fin ) )
19	18	simpld 446	. . . . . . . . . . . . . . . 16 |- ( ph -> G : B --> A )
20		fdm 5554	. . . . . . . . . . . . . . . 16 |- ( G : B --> A -> dom G = B )
21	19, 20	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> dom G = B )
22	15, 21	syl5sseq 3356	. . . . . . . . . . . . . 14 |- ( ph -> ( `' G " ( _V \ 1o ) ) C_ B )
23		cnvexg 5364	. . . . . . . . . . . . . . . . . . 19 |- ( G e. S -> `' G e. _V )
24	16, 23	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> `' G e. _V )
25		imaexg 5176	. . . . . . . . . . . . . . . . . 18 |- ( `' G e. _V -> ( `' G " ( _V \ 1o ) ) e. _V )
26		cantnflem1.o	. . . . . . . . . . . . . . . . . . 19 |- O = OrdIso ( _E , ( `' G " ( _V \ 1o ) ) )
27	26	oion 7461	. . . . . . . . . . . . . . . . . 18 |- ( ( `' G " ( _V \ 1o ) ) e. _V -> dom O e. On )
28	24, 25, 27	3syl 19	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom O e. On )
29		uniexg 4665	. . . . . . . . . . . . . . . . 17 |- ( dom O e. On -> U. dom O e. _V )
30		sucidg 4619	. . . . . . . . . . . . . . . . 17 |- ( U. dom O e. _V -> U. dom O e. suc U. dom O )
31	28, 29, 30	3syl 19	. . . . . . . . . . . . . . . 16 |- ( ph -> U. dom O e. suc U. dom O )
32		oemapval.t	. . . . . . . . . . . . . . . . . . . . . 22 |- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
33		oemapvali.5	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> F T G )
34		oemapvali.6	. . . . . . . . . . . . . . . . . . . . . 22 |- X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
35	2, 3, 4, 32, 1, 16, 33, 34	cantnflem1a 7597	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> X e. ( `' G " ( _V \ 1o ) ) )
36		n0i 3593	. . . . . . . . . . . . . . . . . . . . 21 |- ( X e. ( `' G " ( _V \ 1o ) ) -> -. ( `' G " ( _V \ 1o ) ) = (/) )
37	35, 36	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> -. ( `' G " ( _V \ 1o ) ) = (/) )
38	4, 22	ssexd 4310	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( `' G " ( _V \ 1o ) ) e. _V )
39	2, 3, 4, 26, 16	cantnfcl 7578	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( _E We ( `' G " ( _V \ 1o ) ) /\ dom O e. om ) )
40	39	simpld 446	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> _E We ( `' G " ( _V \ 1o ) ) )
41	26	oien 7463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( `' G " ( _V \ 1o ) ) e. _V /\ _E We ( `' G " ( _V \ 1o ) ) ) -> dom O ~~ ( `' G " ( _V \ 1o ) ) )
42	38, 40, 41	syl2anc 643	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> dom O ~~ ( `' G " ( _V \ 1o ) ) )
43		breq1 4175	. . . . . . . . . . . . . . . . . . . . . 22 |- ( dom O = (/) -> ( dom O ~~ ( `' G " ( _V \ 1o ) ) <-> (/) ~~ ( `' G " ( _V \ 1o ) ) ) )
44		ensymb 7114	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( (/) ~~ ( `' G " ( _V \ 1o ) ) <-> ( `' G " ( _V \ 1o ) ) ~~ (/) )
45		en0 7129	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( `' G " ( _V \ 1o ) ) ~~ (/) <-> ( `' G " ( _V \ 1o ) ) = (/) )
46	44, 45	bitri 241	. . . . . . . . . . . . . . . . . . . . . 22 |- ( (/) ~~ ( `' G " ( _V \ 1o ) ) <-> ( `' G " ( _V \ 1o ) ) = (/) )
47	43, 46	syl6bb 253	. . . . . . . . . . . . . . . . . . . . 21 |- ( dom O = (/) -> ( dom O ~~ ( `' G " ( _V \ 1o ) ) <-> ( `' G " ( _V \ 1o ) ) = (/) ) )
48	42, 47	syl5ibcom 212	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( dom O = (/) -> ( `' G " ( _V \ 1o ) ) = (/) ) )
49	37, 48	mtod 170	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> -. dom O = (/) )
50	39	simprd 450	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> dom O e. om )
51		nnlim 4817	. . . . . . . . . . . . . . . . . . . 20 |- ( dom O e. om -> -. Lim dom O )
52	50, 51	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> -. Lim dom O )
53		ioran 477	. . . . . . . . . . . . . . . . . . 19 |- ( -. ( dom O = (/) \/ Lim dom O ) <-> ( -. dom O = (/) /\ -. Lim dom O ) )
54	49, 52, 53	sylanbrc 646	. . . . . . . . . . . . . . . . . 18 |- ( ph -> -. ( dom O = (/) \/ Lim dom O ) )
55	26	oicl 7454	. . . . . . . . . . . . . . . . . . 19 |- Ord dom O
56		unizlim 4657	. . . . . . . . . . . . . . . . . . 19 |- ( Ord dom O -> ( dom O = U. dom O <-> ( dom O = (/) \/ Lim dom O ) ) )
57	55, 56	mp1i 12	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( dom O = U. dom O <-> ( dom O = (/) \/ Lim dom O ) ) )
58	54, 57	mtbird 293	. . . . . . . . . . . . . . . . 17 |- ( ph -> -. dom O = U. dom O )
59		orduniorsuc 4769	. . . . . . . . . . . . . . . . . . 19 |- ( Ord dom O -> ( dom O = U. dom O \/ dom O = suc U. dom O ) )
60	55, 59	mp1i 12	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( dom O = U. dom O \/ dom O = suc U. dom O ) )
61	60	ord 367	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( -. dom O = U. dom O -> dom O = suc U. dom O ) )
62	58, 61	mpd 15	. . . . . . . . . . . . . . . 16 |- ( ph -> dom O = suc U. dom O )
63	31, 62	eleqtrrd 2481	. . . . . . . . . . . . . . 15 |- ( ph -> U. dom O e. dom O )
64	26	oif 7455	. . . . . . . . . . . . . . . 16 |- O : dom O --> ( `' G " ( _V \ 1o ) )
65	64	ffvelrni 5828	. . . . . . . . . . . . . . 15 |- ( U. dom O e. dom O -> ( O ` U. dom O ) e. ( `' G " ( _V \ 1o ) ) )
66	63, 65	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( O ` U. dom O ) e. ( `' G " ( _V \ 1o ) ) )
67	22, 66	sseldd 3309	. . . . . . . . . . . . 13 |- ( ph -> ( O ` U. dom O ) e. B )
68		onelon 4566	. . . . . . . . . . . . 13 |- ( ( B e. On /\ ( O ` U. dom O ) e. B ) -> ( O ` U. dom O ) e. On )
69	4, 67, 68	syl2anc 643	. . . . . . . . . . . 12 |- ( ph -> ( O ` U. dom O ) e. On )
70	69	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ x e. B ) -> ( O ` U. dom O ) e. On )
71		ontri1 4575	. . . . . . . . . . 11 |- ( ( x e. On /\ ( O ` U. dom O ) e. On ) -> ( x C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. x ) )
72	14, 70, 71	syl2anc 643	. . . . . . . . . 10 |- ( ( ph /\ x e. B ) -> ( x C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. x ) )
73	72	con2bid 320	. . . . . . . . 9 |- ( ( ph /\ x e. B ) -> ( ( O ` U. dom O ) e. x <-> -. x C_ ( O ` U. dom O ) ) )
74		simprl 733	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> x e. B )
75	2, 3, 4, 32, 1, 16, 33, 34	oemapvali 7596	. . . . . . . . . . . . . 14 |- ( ph -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) )
76	75	simp3d 971	. . . . . . . . . . . . 13 |- ( ph -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) )
77	76	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) )
78	26	oiiso 7462	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( `' G " ( _V \ 1o ) ) e. _V /\ _E We ( `' G " ( _V \ 1o ) ) ) -> O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) )
79	38, 40, 78	syl2anc 643	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) )
80		isof1o 6004	. . . . . . . . . . . . . . . . . . . . 21 |- ( O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) -> O : dom O -1-1-onto-> ( `' G " ( _V \ 1o ) ) )
81	79, 80	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> O : dom O -1-1-onto-> ( `' G " ( _V \ 1o ) ) )
82		f1ocnv 5646	. . . . . . . . . . . . . . . . . . . 20 |- ( O : dom O -1-1-onto-> ( `' G " ( _V \ 1o ) ) -> `' O : ( `' G " ( _V \ 1o ) ) -1-1-onto-> dom O )
83		f1of 5633	. . . . . . . . . . . . . . . . . . . 20 |- ( `' O : ( `' G " ( _V \ 1o ) ) -1-1-onto-> dom O -> `' O : ( `' G " ( _V \ 1o ) ) --> dom O )
84	81, 82, 83	3syl 19	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> `' O : ( `' G " ( _V \ 1o ) ) --> dom O )
85	84, 35	ffvelrnd 5830	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( `' O ` X ) e. dom O )
86		elssuni 4003	. . . . . . . . . . . . . . . . . 18 |- ( ( `' O ` X ) e. dom O -> ( `' O ` X ) C_ U. dom O )
87	85, 86	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( `' O ` X ) C_ U. dom O )
88		ordelon 4565	. . . . . . . . . . . . . . . . . . . 20 |- ( ( Ord dom O /\ ( `' O ` X ) e. dom O ) -> ( `' O ` X ) e. On )
89	55, 85, 88	sylancr 645	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( `' O ` X ) e. On )
90		eloni 4551	. . . . . . . . . . . . . . . . . . 19 |- ( ( `' O ` X ) e. On -> Ord ( `' O ` X ) )
91	89, 90	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> Ord ( `' O ` X ) )
92		orduni 4733	. . . . . . . . . . . . . . . . . . 19 |- ( Ord dom O -> Ord U. dom O )
93	55, 92	ax-mp 8	. . . . . . . . . . . . . . . . . 18 |- Ord U. dom O
94		ordtri1 4574	. . . . . . . . . . . . . . . . . 18 |- ( ( Ord ( `' O ` X ) /\ Ord U. dom O ) -> ( ( `' O ` X ) C_ U. dom O <-> -. U. dom O e. ( `' O ` X ) ) )
95	91, 93, 94	sylancl 644	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( `' O ` X ) C_ U. dom O <-> -. U. dom O e. ( `' O ` X ) ) )
96	87, 95	mpbid 202	. . . . . . . . . . . . . . . 16 |- ( ph -> -. U. dom O e. ( `' O ` X ) )
97		isorel 6005	. . . . . . . . . . . . . . . . . . 19 |- ( ( O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) /\ ( U. dom O e. dom O /\ ( `' O ` X ) e. dom O ) ) -> ( U. dom O _E ( `' O ` X ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) ) )
98	79, 63, 85, 97	syl12anc 1182	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( U. dom O _E ( `' O ` X ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) ) )
99		fvex 5701	. . . . . . . . . . . . . . . . . . 19 |- ( `' O ` X ) e. _V
100	99	epelc 4456	. . . . . . . . . . . . . . . . . 18 |- ( U. dom O _E ( `' O ` X ) <-> U. dom O e. ( `' O ` X ) )
101		fvex 5701	. . . . . . . . . . . . . . . . . . 19 |- ( O ` ( `' O ` X ) ) e. _V
102	101	epelc 4456	. . . . . . . . . . . . . . . . . 18 |- ( ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) )
103	98, 100, 102	3bitr3g 279	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( U. dom O e. ( `' O ` X ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) ) )
104		f1ocnvfv2 5974	. . . . . . . . . . . . . . . . . . 19 |- ( ( O : dom O -1-1-onto-> ( `' G " ( _V \ 1o ) ) /\ X e. ( `' G " ( _V \ 1o ) ) ) -> ( O ` ( `' O ` X ) ) = X )
105	81, 35, 104	syl2anc 643	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( O ` ( `' O ` X ) ) = X )
106	105	eleq2d 2471	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) <-> ( O ` U. dom O ) e. X ) )
107	103, 106	bitrd 245	. . . . . . . . . . . . . . . 16 |- ( ph -> ( U. dom O e. ( `' O ` X ) <-> ( O ` U. dom O ) e. X ) )
108	96, 107	mtbid 292	. . . . . . . . . . . . . . 15 |- ( ph -> -. ( O ` U. dom O ) e. X )
109	75	simp1d 969	. . . . . . . . . . . . . . . . 17 |- ( ph -> X e. B )
110		onelon 4566	. . . . . . . . . . . . . . . . 17 |- ( ( B e. On /\ X e. B ) -> X e. On )
111	4, 109, 110	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ph -> X e. On )
112		ontri1 4575	. . . . . . . . . . . . . . . 16 |- ( ( X e. On /\ ( O ` U. dom O ) e. On ) -> ( X C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. X ) )
113	111, 69, 112	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ph -> ( X C_ ( O ` U. dom O ) <-> -. ( O ` U. dom O ) e. X ) )
114	108, 113	mpbird 224	. . . . . . . . . . . . . 14 |- ( ph -> X C_ ( O ` U. dom O ) )
115	114	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> X C_ ( O ` U. dom O ) )
116		simprr 734	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( O ` U. dom O ) e. x )
117	111	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> X e. On )
118	14	adantrr 698	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> x e. On )
119		ontr2 4588	. . . . . . . . . . . . . 14 |- ( ( X e. On /\ x e. On ) -> ( ( X C_ ( O ` U. dom O ) /\ ( O ` U. dom O ) e. x ) -> X e. x ) )
120	117, 118, 119	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( ( X C_ ( O ` U. dom O ) /\ ( O ` U. dom O ) e. x ) -> X e. x ) )
121	115, 116, 120	mp2and 661	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> X e. x )
122		eleq2 2465	. . . . . . . . . . . . . 14 |- ( w = x -> ( X e. w <-> X e. x ) )
123		fveq2 5687	. . . . . . . . . . . . . . 15 |- ( w = x -> ( F ` w ) = ( F ` x ) )
124		fveq2 5687	. . . . . . . . . . . . . . 15 |- ( w = x -> ( G ` w ) = ( G ` x ) )
125	123, 124	eqeq12d 2418	. . . . . . . . . . . . . 14 |- ( w = x -> ( ( F ` w ) = ( G ` w ) <-> ( F ` x ) = ( G ` x ) ) )
126	122, 125	imbi12d 312	. . . . . . . . . . . . 13 |- ( w = x -> ( ( X e. w -> ( F ` w ) = ( G ` w ) ) <-> ( X e. x -> ( F ` x ) = ( G ` x ) ) ) )
127	126	rspcv 3008	. . . . . . . . . . . 12 |- ( x e. B -> ( A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) -> ( X e. x -> ( F ` x ) = ( G ` x ) ) ) )
128	74, 77, 121, 127	syl3c 59	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( F ` x ) = ( G ` x ) )
129	116	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( O ` U. dom O ) e. x )
130	79	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) )
131	63	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> U. dom O e. dom O )
132	84	ad2antrr 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> `' O : ( `' G " ( _V \ 1o ) ) --> dom O )
133		ffvelrn 5827	. . . . . . . . . . . . . . . . . . 19 |- ( ( `' O : ( `' G " ( _V \ 1o ) ) --> dom O /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( `' O ` x ) e. dom O )
134	132, 133	sylancom 649	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( `' O ` x ) e. dom O )
135		isorel 6005	. . . . . . . . . . . . . . . . . 18 |- ( ( O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) /\ ( U. dom O e. dom O /\ ( `' O ` x ) e. dom O ) ) -> ( U. dom O _E ( `' O ` x ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` x ) ) ) )
136	130, 131, 134, 135	syl12anc 1182	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( U. dom O _E ( `' O ` x ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` x ) ) ) )
137		fvex 5701	. . . . . . . . . . . . . . . . . 18 |- ( `' O ` x ) e. _V
138	137	epelc 4456	. . . . . . . . . . . . . . . . 17 |- ( U. dom O _E ( `' O ` x ) <-> U. dom O e. ( `' O ` x ) )
139		fvex 5701	. . . . . . . . . . . . . . . . . 18 |- ( O ` ( `' O ` x ) ) e. _V
140	139	epelc 4456	. . . . . . . . . . . . . . . . 17 |- ( ( O ` U. dom O ) _E ( O ` ( `' O ` x ) ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` x ) ) )
141	136, 138, 140	3bitr3g 279	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( U. dom O e. ( `' O ` x ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` x ) ) ) )
142	81	ad2antrr 707	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> O : dom O -1-1-onto-> ( `' G " ( _V \ 1o ) ) )
143		f1ocnvfv2 5974	. . . . . . . . . . . . . . . . . 18 |- ( ( O : dom O -1-1-onto-> ( `' G " ( _V \ 1o ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( O ` ( `' O ` x ) ) = x )
144	142, 143	sylancom 649	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( O ` ( `' O ` x ) ) = x )
145	144	eleq2d 2471	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( ( O ` U. dom O ) e. ( O ` ( `' O ` x ) ) <-> ( O ` U. dom O ) e. x ) )
146	141, 145	bitrd 245	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( U. dom O e. ( `' O ` x ) <-> ( O ` U. dom O ) e. x ) )
147	129, 146	mpbird 224	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> U. dom O e. ( `' O ` x ) )
148		elssuni 4003	. . . . . . . . . . . . . . . 16 |- ( ( `' O ` x ) e. dom O -> ( `' O ` x ) C_ U. dom O )
149	134, 148	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( `' O ` x ) C_ U. dom O )
150		ordelon 4565	. . . . . . . . . . . . . . . . . 18 |- ( ( Ord dom O /\ ( `' O ` x ) e. dom O ) -> ( `' O ` x ) e. On )
151	55, 134, 150	sylancr 645	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( `' O ` x ) e. On )
152		eloni 4551	. . . . . . . . . . . . . . . . 17 |- ( ( `' O ` x ) e. On -> Ord ( `' O ` x ) )
153	151, 152	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> Ord ( `' O ` x ) )
154		ordtri1 4574	. . . . . . . . . . . . . . . 16 |- ( ( Ord ( `' O ` x ) /\ Ord U. dom O ) -> ( ( `' O ` x ) C_ U. dom O <-> -. U. dom O e. ( `' O ` x ) ) )
155	153, 93, 154	sylancl 644	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> ( ( `' O ` x ) C_ U. dom O <-> -. U. dom O e. ( `' O ` x ) ) )
156	149, 155	mpbid 202	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) /\ x e. ( `' G " ( _V \ 1o ) ) ) -> -. U. dom O e. ( `' O ` x ) )
157	147, 156	pm2.65da 560	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> -. x e. ( `' G " ( _V \ 1o ) ) )
158	74, 157	eldifd 3291	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> x e. ( B \ ( `' G " ( _V \ 1o ) ) ) )
159		df1o2 6695	. . . . . . . . . . . . . . . 16 |- 1o = { (/) }
160	159	difeq2i 3422	. . . . . . . . . . . . . . 15 |- ( _V \ 1o ) = ( _V \ { (/) } )
161	160	imaeq2i 5160	. . . . . . . . . . . . . 14 |- ( `' G " ( _V \ 1o ) ) = ( `' G " ( _V \ { (/) } ) )
162		eqimss2 3361	. . . . . . . . . . . . . 14 |- ( ( `' G " ( _V \ 1o ) ) = ( `' G " ( _V \ { (/) } ) ) -> ( `' G " ( _V \ { (/) } ) ) C_ ( `' G " ( _V \ 1o ) ) )
163	161, 162	mp1i 12	. . . . . . . . . . . . 13 |- ( ph -> ( `' G " ( _V \ { (/) } ) ) C_ ( `' G " ( _V \ 1o ) ) )
164	19, 163	suppssr 5823	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( B \ ( `' G " ( _V \ 1o ) ) ) ) -> ( G ` x ) = (/) )
165	158, 164	syldan 457	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( G ` x ) = (/) )
166	128, 165	eqtrd 2436	. . . . . . . . . 10 |- ( ( ph /\ ( x e. B /\ ( O ` U. dom O ) e. x ) ) -> ( F ` x ) = (/) )
167	166	expr 599	. . . . . . . . 9 |- ( ( ph /\ x e. B ) -> ( ( O ` U. dom O ) e. x -> ( F ` x ) = (/) ) )
168	73, 167	sylbird 227	. . . . . . . 8 |- ( ( ph /\ x e. B ) -> ( -. x C_ ( O ` U. dom O ) -> ( F ` x ) = (/) ) )
169	168	imp 419	. . . . . . 7 |- ( ( ( ph /\ x e. B ) /\ -. x C_ ( O ` U. dom O ) ) -> ( F ` x ) = (/) )
170	9, 10, 11, 169	ifbothda 3729	. . . . . 6 |- ( ( ph /\ x e. B ) -> ( F ` x ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) )
171	170	mpteq2dva 4255	. . . . 5 |- ( ph -> ( x e. B |-> ( F ` x ) ) = ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) )
172	8, 171	eqtrd 2436	. . . 4 |- ( ph -> F = ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) )
173	172	fveq2d 5691	. . 3 |- ( ph -> ( ( A CNF B ) ` F ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) )
174	62, 50	eqeltrrd 2479	. . . . . 6 |- ( ph -> suc U. dom O e. om )
175		peano2b 4820	. . . . . 6 |- ( U. dom O e. om <-> suc U. dom O e. om )
176	174, 175	sylibr 204	. . . . 5 |- ( ph -> U. dom O e. om )
177		eleq1 2464	. . . . . . . . 9 |- ( y = U. dom O -> ( y e. dom O <-> U. dom O e. dom O ) )
178		sseq2 3330	. . . . . . . . 9 |- ( y = U. dom O -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ U. dom O ) )
179	177, 178	anbi12d 692	. . . . . . . 8 |- ( y = U. dom O -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) ) )
180		fveq2 5687	. . . . . . . . . . . . 13 |- ( y = U. dom O -> ( O ` y ) = ( O ` U. dom O ) )
181	180	sseq2d 3336	. . . . . . . . . . . 12 |- ( y = U. dom O -> ( x C_ ( O ` y ) <-> x C_ ( O ` U. dom O ) ) )
182	181	ifbid 3717	. . . . . . . . . . 11 |- ( y = U. dom O -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) )
183	182	mpteq2dv 4256	. . . . . . . . . 10 |- ( y = U. dom O -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) )
184	183	fveq2d 5691	. . . . . . . . 9 |- ( y = U. dom O -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) )
185		suceq 4606	. . . . . . . . . 10 |- ( y = U. dom O -> suc y = suc U. dom O )
186	185	fveq2d 5691	. . . . . . . . 9 |- ( y = U. dom O -> ( H ` suc y ) = ( H ` suc U. dom O ) )
187	184, 186	eleq12d 2472	. . . . . . . 8 |- ( y = U. dom O -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) )
188	179, 187	imbi12d 312	. . . . . . 7 |- ( y = U. dom O -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) ) )
189	188	imbi2d 308	. . . . . 6 |- ( y = U. dom O -> ( ( ph -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) ) <-> ( ph -> ( ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc U. dom O ) ) ) ) )
190		eleq1 2464	. . . . . . . . 9 |- ( y = (/) -> ( y e. dom O <-> (/) e. dom O ) )
191		sseq2 3330	. . . . . . . . 9 |- ( y = (/) -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ (/) ) )
192	190, 191	anbi12d 692	. . . . . . . 8 |- ( y = (/) -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) ) )
193		fveq2 5687	. . . . . . . . . . . . 13 |- ( y = (/) -> ( O ` y ) = ( O ` (/) ) )
194	193	sseq2d 3336	. . . . . . . . . . . 12 |- ( y = (/) -> ( x C_ ( O ` y ) <-> x C_ ( O ` (/) ) ) )
195	194	ifbid 3717	. . . . . . . . . . 11 |- ( y = (/) -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) )
196	195	mpteq2dv 4256	. . . . . . . . . 10 |- ( y = (/) -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) )
197	196	fveq2d 5691	. . . . . . . . 9 |- ( y = (/) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) )
198		suceq 4606	. . . . . . . . . 10 |- ( y = (/) -> suc y = suc (/) )
199	198	fveq2d 5691	. . . . . . . . 9 |- ( y = (/) -> ( H ` suc y ) = ( H ` suc (/) ) )
200	197, 199	eleq12d 2472	. . . . . . . 8 |- ( y = (/) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) )
201	192, 200	imbi12d 312	. . . . . . 7 |- ( y = (/) -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) ) )
202		eleq1 2464	. . . . . . . . 9 |- ( y = u -> ( y e. dom O <-> u e. dom O ) )
203		sseq2 3330	. . . . . . . . 9 |- ( y = u -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ u ) )
204	202, 203	anbi12d 692	. . . . . . . 8 |- ( y = u -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( u e. dom O /\ ( `' O ` X ) C_ u ) ) )
205		fveq2 5687	. . . . . . . . . . . . 13 |- ( y = u -> ( O ` y ) = ( O ` u ) )
206	205	sseq2d 3336	. . . . . . . . . . . 12 |- ( y = u -> ( x C_ ( O ` y ) <-> x C_ ( O ` u ) ) )
207	206	ifbid 3717	. . . . . . . . . . 11 |- ( y = u -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) )
208	207	mpteq2dv 4256	. . . . . . . . . 10 |- ( y = u -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) )
209	208	fveq2d 5691	. . . . . . . . 9 |- ( y = u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) )
210		suceq 4606	. . . . . . . . . 10 |- ( y = u -> suc y = suc u )
211	210	fveq2d 5691	. . . . . . . . 9 |- ( y = u -> ( H ` suc y ) = ( H ` suc u ) )
212	209, 211	eleq12d 2472	. . . . . . . 8 |- ( y = u -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) )
213	204, 212	imbi12d 312	. . . . . . 7 |- ( y = u -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( u e. dom O /\ ( `' O ` X ) C_ u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) ) ) )
214		eleq1 2464	. . . . . . . . 9 |- ( y = suc u -> ( y e. dom O <-> suc u e. dom O ) )
215		sseq2 3330	. . . . . . . . 9 |- ( y = suc u -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ suc u ) )
216	214, 215	anbi12d 692	. . . . . . . 8 |- ( y = suc u -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) ) )
217		fveq2 5687	. . . . . . . . . . . . 13 |- ( y = suc u -> ( O ` y ) = ( O ` suc u ) )
218	217	sseq2d 3336	. . . . . . . . . . . 12 |- ( y = suc u -> ( x C_ ( O ` y ) <-> x C_ ( O ` suc u ) ) )
219	218	ifbid 3717	. . . . . . . . . . 11 |- ( y = suc u -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) )
220	219	mpteq2dv 4256	. . . . . . . . . 10 |- ( y = suc u -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) )
221	220	fveq2d 5691	. . . . . . . . 9 |- ( y = suc u -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) )
222		suceq 4606	. . . . . . . . . 10 |- ( y = suc u -> suc y = suc suc u )
223	222	fveq2d 5691	. . . . . . . . 9 |- ( y = suc u -> ( H ` suc y ) = ( H ` suc suc u ) )
224	221, 223	eleq12d 2472	. . . . . . . 8 |- ( y = suc u -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) )
225	216, 224	imbi12d 312	. . . . . . 7 |- ( y = suc u -> ( ( ( y e. dom O /\ ( `' O ` X ) C_ y ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc y ) ) <-> ( ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc suc u ) ) ) )
226	105	sseq2d 3336	. . . . . . . . . . . 12 |- ( ph -> ( x C_ ( O ` ( `' O ` X ) ) <-> x C_ X ) )
227	226	ifbid 3717	. . . . . . . . . . 11 |- ( ph -> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) = if ( x C_ X , ( F ` x ) , (/) ) )
228	227	mpteq2dv 4256	. . . . . . . . . 10 |- ( ph -> ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) )
229	228	fveq2d 5691	. . . . . . . . 9 |- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) )
230		cantnflem1.h	. . . . . . . . . 10 |- H = seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( G ` ( O ` k ) ) ) +o z ) ) , (/) )
231	2, 3, 4, 32, 1, 16, 33, 34, 26, 230	cantnflem1d 7600	. . . . . . . . 9 |- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) )
232	229, 231	eqeltrd 2478	. . . . . . . 8 |- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) )
233		ss0 3618	. . . . . . . . . . . . . . 15 |- ( ( `' O ` X ) C_ (/) -> ( `' O ` X ) = (/) )
234	233	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( ( `' O ` X ) C_ (/) -> ( O ` ( `' O ` X ) ) = ( O ` (/) ) )
235	234	sseq2d 3336	. . . . . . . . . . . . 13 |- ( ( `' O ` X ) C_ (/) -> ( x C_ ( O ` ( `' O ` X ) ) <-> x C_ ( O ` (/) ) ) )
236	235	ifbid 3717	. . . . . . . . . . . 12 |- ( ( `' O ` X ) C_ (/) -> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) )
237	236	mpteq2dv 4256	. . . . . . . . . . 11 |- ( ( `' O ` X ) C_ (/) -> ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) )
238	237	fveq2d 5691	. . . . . . . . . 10 |- ( ( `' O ` X ) C_ (/) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) )
239		suceq 4606	. . . . . . . . . . . 12 |- ( ( `' O ` X ) = (/) -> suc ( `' O ` X ) = suc (/) )
240	233, 239	syl 16	. . . . . . . . . . 11 |- ( ( `' O ` X ) C_ (/) -> suc ( `' O ` X ) = suc (/) )
241	240	fveq2d 5691	. . . . . . . . . 10 |- ( ( `' O ` X ) C_ (/) -> ( H ` suc ( `' O ` X ) ) = ( H ` suc (/) ) )
242	238, 241	eleq12d 2472	. . . . . . . . 9 |- ( ( `' O ` X ) C_ (/) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) )
243	242	adantl 453	. . . . . . . 8 |- ( ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) <-> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) )
244	232, 243	syl5ibcom 212	. . . . . . 7 |- ( ph -> ( ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) )
245	89	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ suc u e. dom O ) -> ( `' O ` X ) e. On )
246	55	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> Ord dom O )
247		ordelon 4565	. . . . . . . . . . . . 13 |- ( ( Ord dom O /\ suc u e. dom O ) -> suc u e. On )
248	246, 247	sylan 458	. . . . . . . . . . . 12 |- ( ( ph /\ suc u e. dom O ) -> suc u e. On )
249		onsseleq 4582	. . . . . . . . . . . 12 |- ( ( ( `' O ` X ) e. On /\ suc u e. On ) -> ( ( `' O ` X ) C_ suc u <-> ( ( `' O ` X ) e. suc u \/ ( `' O ` X ) = suc u ) ) )
250	245, 248, 249	syl2anc 643	. . . . . . . . . . 11 |- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ suc u <-> ( ( `' O ` X ) e. suc u \/ ( `' O ` X ) = suc u ) ) )
251		sucelon 4756	. . . . . . . . . . . . . . . 16 |- ( u e. On <-> suc u e. On )
252	248, 251	sylibr 204	. . . . . . . . . . . . . . 15 |- ( ( ph /\ suc u e. dom O ) -> u e. On )
253		eloni 4551	. . . . . . . . . . . . . . 15 |- ( u e. On -> Ord u )
254	252, 253	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ suc u e. dom O ) -> Ord u )
255		ordsssuc 4627	. . . . . . . . . . . . . 14 |- ( ( ( `' O ` X ) e. On /\ Ord u ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) )
256	245, 254, 255	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) )
257		ordtr 4555	. . . . . . . . . . . . . . . . . 18 |- ( Ord dom O -> Tr dom O )
258	55, 257	mp1i 12	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> Tr dom O )
259		simprl 733	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc u e. dom O )
260		trsuc 4625	. . . . . . . . . . . . . . . . 17 |- ( ( Tr dom O /\ suc u e. dom O ) -> u e. dom O )
261	258, 259, 260	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> u e. dom O )
262		simprr 734	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' O ` X ) C_ u )
263	261, 262	jca 519	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u e. dom O /\ ( `' O ` X ) C_ u ) )
264	3	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> A e. On )
265	4	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> B e. On )
266		oecl 6740	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
267	264, 265, 266	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A ^o B ) e. On )
268	2, 264, 265	cantnff 7585	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A CNF B ) : S --> ( A ^o B ) )
269	7	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ x e. B ) -> ( F ` x ) e. A )
270	19, 109	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( G ` X ) e. A )
271		ne0i 3594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( G ` X ) e. A -> A =/= (/) )
272	270, 271	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> A =/= (/) )
273		on0eln0 4596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
274	3, 273	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( (/) e. A <-> A =/= (/) ) )
275	272, 274	mpbird 224	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> (/) e. A )
276	275	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ x e. B ) -> (/) e. A )
277		ifcl 3735	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( F ` x ) e. A /\ (/) e. A ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. A )
278	269, 276, 277	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. B ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. A )
279		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) )
280	278, 279	fmptd 5852	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) : B --> A )
281	6	simprd 450	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( `' F " ( _V \ 1o ) ) e. Fin )
282	160	imaeq2i 5160	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( `' ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) " ( _V \ 1o ) ) = ( `' ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) " ( _V \ { (/) } ) )
283	160	imaeq2i 5160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( `' F " ( _V \ 1o ) ) = ( `' F " ( _V \ { (/) } ) )
284		eqimss2 3361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( `' F " ( _V \ 1o ) ) = ( `' F " ( _V \ { (/) } ) ) -> ( `' F " ( _V \ { (/) } ) ) C_ ( `' F " ( _V \ 1o ) ) )
285	283, 284	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( `' F " ( _V \ { (/) } ) ) C_ ( `' F " ( _V \ 1o ) ) )
286	7, 285	suppssr 5823	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ x e. ( B \ ( `' F " ( _V \ 1o ) ) ) ) -> ( F ` x ) = (/) )
287	286	ifeq1d 3713	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ x e. ( B \ ( `' F " ( _V \ 1o ) ) ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , (/) , (/) ) )
288		ifid 3731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- if ( x C_ ( O ` u ) , (/) , (/) ) = (/)
289	287, 288	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ x e. ( B \ ( `' F " ( _V \ 1o ) ) ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = (/) )
290	289	suppss2 6259	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( `' ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) " ( _V \ { (/) } ) ) C_ ( `' F " ( _V \ 1o ) ) )
291	282, 290	syl5eqss 3352	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( `' ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) " ( _V \ 1o ) ) C_ ( `' F " ( _V \ 1o ) ) )
292		ssfi 7288	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( `' F " ( _V \ 1o ) ) e. Fin /\ ( `' ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) " ( _V \ 1o ) ) C_ ( `' F " ( _V \ 1o ) ) ) -> ( `' ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) " ( _V \ 1o ) ) e. Fin )
293	281, 291, 292	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( `' ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) " ( _V \ 1o ) ) e. Fin )
294	2, 3, 4	cantnfs 7577	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S <-> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) : B --> A /\ ( `' ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) " ( _V \ 1o ) ) e. Fin ) ) )
295	280, 293, 294	mpbir2and 889	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S )
296	295	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S )
297	268, 296	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( A ^o B ) )
298		onelon 4566	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A ^o B ) e. On /\ ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( A ^o B ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. On )
299	267, 297, 298	syl2anc 643	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. On )
300	50	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> dom O e. om )
301		elnn 4814	. . . . . . . . . . . . . . . . . . . 20 |- ( ( suc u e. dom O /\ dom O e. om ) -> suc u e. om )
302	259, 300, 301	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc u e. om )
303	230	cantnfvalf 7576	. . . . . . . . . . . . . . . . . . . 20 |- H : om --> On
304	303	ffvelrni 5828	. . . . . . . . . . . . . . . . . . 19 |- ( suc u e. om -> ( H ` suc u ) e. On )
305	302, 304	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( H ` suc u ) e. On )
306	22	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' G " ( _V \ 1o ) ) C_ B )
307	64	ffvelrni 5828	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( suc u e. dom O -> ( O ` suc u ) e. ( `' G " ( _V \ 1o ) ) )
308	259, 307	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. ( `' G " ( _V \ 1o ) ) )
309	306, 308	sseldd 3309	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. B )
310		onelon 4566	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( B e. On /\ ( O ` suc u ) e. B ) -> ( O ` suc u ) e. On )
311	265, 309, 310	syl2anc 643	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. On )
312		oecl 6740	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. On /\ ( O ` suc u ) e. On ) -> ( A ^o ( O ` suc u ) ) e. On )
313	264, 311, 312	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A ^o ( O ` suc u ) ) e. On )
314	7	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> F : B --> A )
315	314, 309	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( F ` ( O ` suc u ) ) e. A )
316		onelon 4566	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. On /\ ( F ` ( O ` suc u ) ) e. A ) -> ( F ` ( O ` suc u ) ) e. On )
317	264, 315, 316	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( F ` ( O ` suc u ) ) e. On )
318		omcl 6739	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A ^o ( O ` suc u ) ) e. On /\ ( F ` ( O ` suc u ) ) e. On ) -> ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) e. On )
319	313, 317, 318	syl2anc 643	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) e. On )
320		oaord 6749	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. On /\ ( H ` suc u ) e. On /\ ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) e. On ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) <-> ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) e. ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) )
321	299, 305, 319, 320	syl3anc 1184	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc u ) <-> ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) e. ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( H ` suc u ) ) ) )
322		ifeq1 3703	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F ` x ) = (/) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` suc u ) , (/) , (/) ) )
323		ifid 3731	. . . . . . . . . . . . . . . . . . . . . . . 24 |- if ( x C_ ( O ` suc u ) , (/) , (/) ) = (/)
324	322, 323	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F ` x ) = (/) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = (/) )
325		ifeq1 3703	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F ` x ) = (/) -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , (/) , (/) ) )
326		ifid 3731	. . . . . . . . . . . . . . . . . . . . . . . 24 |- if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , (/) , (/) ) = (/)
327	325, 326	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F ` x ) = (/) -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = (/) )
328	324, 327	eqeq12d 2418	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( F ` x ) = (/) -> ( if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) <-> (/) = (/) ) )
329	14	adantlr 696	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> x e. On )
330	311	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( O ` suc u ) e. On )
331		onsseleq 4582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. On /\ ( O ` suc u ) e. On ) -> ( x C_ ( O ` suc u ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) )
332	329, 330, 331	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( x C_ ( O ` suc u ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) )
333	332	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` suc u ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) )
334	329	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> x e. On )
335	64	ffvelrni 5828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( u e. dom O -> ( O ` u ) e. ( `' G " ( _V \ 1o ) ) )
336	261, 335	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. ( `' G " ( _V \ 1o ) ) )
337	306, 336	sseldd 3309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. B )
338		onelon 4566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( B e. On /\ ( O ` u ) e. B ) -> ( O ` u ) e. On )
339	265, 337, 338	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. On )
340	339	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( O ` u ) e. On )
341		onsssuc 4628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x e. On /\ ( O ` u ) e. On ) -> ( x C_ ( O ` u ) <-> x e. suc ( O ` u ) ) )
342	334, 340, 341	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> x e. suc ( O ` u ) ) )
343		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- u e. _V
344	343	sucid 4620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- u e. suc u
345	79	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) )
346		isorel 6005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) /\ ( u e. dom O /\ suc u e. dom O ) ) -> ( u _E suc u <-> ( O ` u ) _E ( O ` suc u ) ) )
347	345, 261, 259, 346	syl12anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u _E suc u <-> ( O ` u ) _E ( O ` suc u ) ) )
348	343	sucex 4750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- suc u e. _V
349	348	epelc 4456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( u _E suc u <-> u e. suc u )
350		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( O ` suc u ) e. _V
351	350	epelc 4456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( O ` u ) _E ( O ` suc u ) <-> ( O ` u ) e. ( O ` suc u ) )
352	347, 349, 351	3bitr3g 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u e. suc u <-> ( O ` u ) e. ( O ` suc u ) ) )
353	344, 352	mpbii 203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. ( O ` suc u ) )
354		eloni 4551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( O ` suc u ) e. On -> Ord ( O ` suc u ) )
355	311, 354	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> Ord ( O ` suc u ) )
356		ordelsuc 4759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( O ` u ) e. On /\ Ord ( O ` suc u ) ) -> ( ( O ` u ) e. ( O ` suc u ) <-> suc ( O ` u ) C_ ( O ` suc u ) ) )
357	339, 355, 356	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( O ` u ) e. ( O ` suc u ) <-> suc ( O ` u ) C_ ( O ` suc u ) ) )
358	353, 357	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc ( O ` u ) C_ ( O ` suc u ) )
359	358	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> suc ( O ` u ) C_ ( O ` suc u ) )
360	359	sseld 3307	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. suc ( O ` u ) -> x e. ( O ` suc u ) ) )
361	342, 360	sylbid 207	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) -> x e. ( O ` suc u ) ) )
362		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` u ) e. x )
363	345	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) )
364	363, 80	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> O : dom O -1-1-onto-> ( `' G " ( _V \ 1o ) ) )
365	2, 3, 4, 32, 1, 16, 33, 34, 26	cantnflem1c 7599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. ( `' G " ( _V \ 1o ) ) )
366	364, 365, 143	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` ( `' O ` x ) ) = x )
367	362, 366	eleqtrrd 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` u ) e. ( O ` ( `' O ` x ) ) )
368	261	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> u e. dom O )
369	364, 82, 83	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> `' O : ( `' G " ( _V \ 1o ) ) --> dom O )
370	369, 365	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( `' O ` x ) e. dom O )
371		isorel 6005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) /\ ( u e. dom O /\ ( `' O ` x ) e. dom O ) ) -> ( u _E ( `' O ` x ) <-> ( O ` u ) _E ( O ` ( `' O ` x ) ) ) )
372	363, 368, 370, 371	syl12anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( u _E ( `' O ` x ) <-> ( O ` u ) _E ( O ` ( `' O ` x ) ) ) )
373	137	epelc 4456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( u _E ( `' O ` x ) <-> u e. ( `' O ` x ) )
374	139	epelc 4456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( O ` u ) _E ( O ` ( `' O ` x ) ) <-> ( O ` u ) e. ( O ` ( `' O ` x ) ) )
375	372, 373, 374	3bitr3g 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( u e. ( `' O ` x ) <-> ( O ` u ) e. ( O ` ( `' O ` x ) ) ) )
376	367, 375	mpbird 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> u e. ( `' O ` x ) )
377	55, 370, 150	sylancr 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( `' O ` x ) e. On )
378	377, 152	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> Ord ( `' O ` x ) )
379		ordelsuc 4759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( u e. ( `' O ` x ) /\ Ord ( `' O ` x ) ) -> ( u e. ( `' O ` x ) <-> suc u C_ ( `' O ` x ) ) )
380	376, 378, 379	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( u e. ( `' O ` x ) <-> suc u C_ ( `' O ` x ) ) )
381	376, 380	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u C_ ( `' O ` x ) )
382	259	ad2antrr 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u e. dom O )
383	55, 382, 247	sylancr 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u e. On )
384		ontri1 4575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( suc u e. On /\ ( `' O ` x ) e. On ) -> ( suc u C_ ( `' O ` x ) <-> -. ( `' O ` x ) e. suc u ) )
385	383, 377, 384	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( suc u C_ ( `' O ` x ) <-> -. ( `' O ` x ) e. suc u ) )
386	381, 385	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> -. ( `' O ` x ) e. suc u )
387		isorel 6005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( O Isom _E , _E ( dom O , ( `' G " ( _V \ 1o ) ) ) /\ ( ( `' O ` x ) e. dom O /\ suc u e. dom O ) ) -> ( ( `' O ` x ) _E suc u <-> ( O ` ( `' O ` x ) ) _E ( O ` suc u ) ) )
388	363, 370, 382, 387	syl12anc 1182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( `' O ` x ) _E suc u <-> ( O ` ( `' O ` x ) ) _E ( O ` suc u ) ) )
389	348	epelc 4456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( `' O ` x ) _E suc u <-> ( `' O ` x ) e. suc u )
390	350	epelc 4456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( O ` ( `' O ` x ) ) _E ( O ` suc u ) <-> ( O ` ( `' O ` x ) ) e. ( O ` suc u ) )
391	388, 389, 390	3bitr3g 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( `' O ` x ) e. suc u <-> ( O ` ( `' O ` x ) ) e. ( O ` suc u ) ) )
392	366	eleq1d 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( O ` ( `' O ` x ) ) e. ( O ` suc u ) <-> x e. ( O ` suc u ) ) )
393	391, 392	bitrd 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( ( `' O ` x ) e. suc u <-> x e. ( O ` suc u ) ) )
394	386, 393	mtbid 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> -. x e. ( O ` suc u ) )
395	394	expr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( ( O ` u ) e. x -> -. x e. ( O ` suc u ) ) )
396	395	con2d 109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. ( O ` suc u ) -> -. ( O ` u ) e. x ) )
397		ontri1 4575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x e. On /\ ( O ` u ) e. On ) -> ( x C_ ( O ` u ) <-> -. ( O ` u ) e. x ) )
398	334, 340, 397	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> -. ( O ` u ) e. x ) )
399	396, 398	sylibrd 226	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. ( O ` suc u ) -> x C_ ( O ` u ) ) )
400	361, 399	impbid 184	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> x e. ( O ` suc u ) ) )
401	400	orbi1d 684	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( ( x C_ ( O ` u ) \/ x = ( O ` suc u ) ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) )
402	333, 401	bitr4d 248	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` suc u ) <-> ( x C_ ( O ` u ) \/ x = ( O ` suc u ) ) ) )
403		orcom 377	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x C_ ( O ` u ) \/ x = ( O ` suc u ) ) <-> ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) )
404	402, 403	syl6bb 253	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` suc u ) <-> ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) ) )
405	404	ifbid 3717	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_