Theorem cantnflem1 8011

Description: Lemma for cantnf 8015. 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.) (Revised by AV, 2-Jul-2019.)

Hypotheses

Ref	Expression
cantnfs.s	|- S = dom ( A CNF B )
cantnfs.a	|- ( ph -> A e. On )
cantnfs.b	|- ( 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.f	|- ( ph -> F e. S )
oemapval.g	|- ( ph -> G e. S )
oemapvali.r	|- ( ph -> F T G )
oemapvali.x	|- X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
cantnflem1.o	|- O = OrdIso ( _E , ( G supp (/) ) )
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		ovex 6228	. . . . . 6 |- ( G supp (/) ) e. _V
2		cantnflem1.o	. . . . . . 7 |- O = OrdIso ( _E , ( G supp (/) ) )
3	2	oion 7864	. . . . . 6 |- ( ( G supp (/) ) e. _V -> dom O e. On )
4	1, 3	mp1i 12	. . . . 5 |- ( ph -> dom O e. On )
5		uniexg 6490	. . . . 5 |- ( dom O e. On -> U. dom O e. _V )
6		sucidg 4908	. . . . 5 |- ( U. dom O e. _V -> U. dom O e. suc U. dom O )
7	4, 5, 6	3syl 20	. . . 4 |- ( ph -> U. dom O e. suc U. dom O )
8		cantnfs.s	. . . . . . . . . 10 |- S = dom ( A CNF B )
9		cantnfs.a	. . . . . . . . . 10 |- ( ph -> A e. On )
10		cantnfs.b	. . . . . . . . . 10 |- ( ph -> B e. On )
11		oemapval.t	. . . . . . . . . 10 |- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
12		oemapval.f	. . . . . . . . . 10 |- ( ph -> F e. S )
13		oemapval.g	. . . . . . . . . 10 |- ( ph -> G e. S )
14		oemapvali.r	. . . . . . . . . 10 |- ( ph -> F T G )
15		oemapvali.x	. . . . . . . . . 10 |- X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
16	8, 9, 10, 11, 12, 13, 14, 15	cantnflem1a 8007	. . . . . . . . 9 |- ( ph -> X e. ( G supp (/) ) )
17		n0i 3753	. . . . . . . . 9 |- ( X e. ( G supp (/) ) -> -. ( G supp (/) ) = (/) )
18	16, 17	syl 16	. . . . . . . 8 |- ( ph -> -. ( G supp (/) ) = (/) )
19		suppssdm 6816	. . . . . . . . . . . 12 |- ( G supp (/) ) C_ dom G
20	8, 9, 10	cantnfs 7988	. . . . . . . . . . . . . . 15 |- ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
21	13, 20	mpbid 210	. . . . . . . . . . . . . 14 |- ( ph -> ( G : B --> A /\ G finSupp (/) ) )
22	21	simpld 459	. . . . . . . . . . . . 13 |- ( ph -> G : B --> A )
23		fdm 5674	. . . . . . . . . . . . 13 |- ( G : B --> A -> dom G = B )
24	22, 23	syl 16	. . . . . . . . . . . 12 |- ( ph -> dom G = B )
25	19, 24	syl5sseq 3515	. . . . . . . . . . 11 |- ( ph -> ( G supp (/) ) C_ B )
26	10, 25	ssexd 4550	. . . . . . . . . 10 |- ( ph -> ( G supp (/) ) e. _V )
27	8, 9, 10, 2, 13	cantnfcl 7989	. . . . . . . . . . 11 |- ( ph -> ( _E We ( G supp (/) ) /\ dom O e. om ) )
28	27	simpld 459	. . . . . . . . . 10 |- ( ph -> _E We ( G supp (/) ) )
29	2	oien 7866	. . . . . . . . . 10 |- ( ( ( G supp (/) ) e. _V /\ _E We ( G supp (/) ) ) -> dom O ~~ ( G supp (/) ) )
30	26, 28, 29	syl2anc 661	. . . . . . . . 9 |- ( ph -> dom O ~~ ( G supp (/) ) )
31		breq1 4406	. . . . . . . . . 10 |- ( dom O = (/) -> ( dom O ~~ ( G supp (/) ) <-> (/) ~~ ( G supp (/) ) ) )
32		ensymb 7470	. . . . . . . . . . 11 |- ( (/) ~~ ( G supp (/) ) <-> ( G supp (/) ) ~~ (/) )
33		en0 7485	. . . . . . . . . . 11 |- ( ( G supp (/) ) ~~ (/) <-> ( G supp (/) ) = (/) )
34	32, 33	bitri 249	. . . . . . . . . 10 |- ( (/) ~~ ( G supp (/) ) <-> ( G supp (/) ) = (/) )
35	31, 34	syl6bb 261	. . . . . . . . 9 |- ( dom O = (/) -> ( dom O ~~ ( G supp (/) ) <-> ( G supp (/) ) = (/) ) )
36	30, 35	syl5ibcom 220	. . . . . . . 8 |- ( ph -> ( dom O = (/) -> ( G supp (/) ) = (/) ) )
37	18, 36	mtod 177	. . . . . . 7 |- ( ph -> -. dom O = (/) )
38	27	simprd 463	. . . . . . . 8 |- ( ph -> dom O e. om )
39		nnlim 6602	. . . . . . . 8 |- ( dom O e. om -> -. Lim dom O )
40	38, 39	syl 16	. . . . . . 7 |- ( ph -> -. Lim dom O )
41		ioran 490	. . . . . . 7 |- ( -. ( dom O = (/) \/ Lim dom O ) <-> ( -. dom O = (/) /\ -. Lim dom O ) )
42	37, 40, 41	sylanbrc 664	. . . . . 6 |- ( ph -> -. ( dom O = (/) \/ Lim dom O ) )
43	2	oicl 7857	. . . . . . 7 |- Ord dom O
44		unizlim 4946	. . . . . . 7 |- ( Ord dom O -> ( dom O = U. dom O <-> ( dom O = (/) \/ Lim dom O ) ) )
45	43, 44	mp1i 12	. . . . . 6 |- ( ph -> ( dom O = U. dom O <-> ( dom O = (/) \/ Lim dom O ) ) )
46	42, 45	mtbird 301	. . . . 5 |- ( ph -> -. dom O = U. dom O )
47		orduniorsuc 6554	. . . . . . 7 |- ( Ord dom O -> ( dom O = U. dom O \/ dom O = suc U. dom O ) )
48	43, 47	mp1i 12	. . . . . 6 |- ( ph -> ( dom O = U. dom O \/ dom O = suc U. dom O ) )
49	48	ord 377	. . . . 5 |- ( ph -> ( -. dom O = U. dom O -> dom O = suc U. dom O ) )
50	46, 49	mpd 15	. . . 4 |- ( ph -> dom O = suc U. dom O )
51	7, 50	eleqtrrd 2545	. . 3 |- ( ph -> U. dom O e. dom O )
52	2	oiiso 7865	. . . . . . . 8 |- ( ( ( G supp (/) ) e. _V /\ _E We ( G supp (/) ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
53	26, 28, 52	syl2anc 661	. . . . . . 7 |- ( ph -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
54		isof1o 6128	. . . . . . 7 |- ( O Isom _E , _E ( dom O , ( G supp (/) ) ) -> O : dom O -1-1-onto-> ( G supp (/) ) )
55	53, 54	syl 16	. . . . . 6 |- ( ph -> O : dom O -1-1-onto-> ( G supp (/) ) )
56		f1ocnv 5764	. . . . . 6 |- ( O : dom O -1-1-onto-> ( G supp (/) ) -> `' O : ( G supp (/) ) -1-1-onto-> dom O )
57		f1of 5752	. . . . . 6 |- ( `' O : ( G supp (/) ) -1-1-onto-> dom O -> `' O : ( G supp (/) ) --> dom O )
58	55, 56, 57	3syl 20	. . . . 5 |- ( ph -> `' O : ( G supp (/) ) --> dom O )
59	58, 16	ffvelrnd 5956	. . . 4 |- ( ph -> ( `' O ` X ) e. dom O )
60		elssuni 4232	. . . 4 |- ( ( `' O ` X ) e. dom O -> ( `' O ` X ) C_ U. dom O )
61	59, 60	syl 16	. . 3 |- ( ph -> ( `' O ` X ) C_ U. dom O )
62	50, 38	eqeltrrd 2543	. . . . 5 |- ( ph -> suc U. dom O e. om )
63		peano2b 6605	. . . . 5 |- ( U. dom O e. om <-> suc U. dom O e. om )
64	62, 63	sylibr 212	. . . 4 |- ( ph -> U. dom O e. om )
65		eleq1 2526	. . . . . . . 8 |- ( y = U. dom O -> ( y e. dom O <-> U. dom O e. dom O ) )
66		sseq2 3489	. . . . . . . 8 |- ( y = U. dom O -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ U. dom O ) )
67	65, 66	anbi12d 710	. . . . . . 7 |- ( y = U. dom O -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( U. dom O e. dom O /\ ( `' O ` X ) C_ U. dom O ) ) )
68		fveq2 5802	. . . . . . . . . . . 12 |- ( y = U. dom O -> ( O ` y ) = ( O ` U. dom O ) )
69	68	sseq2d 3495	. . . . . . . . . . 11 |- ( y = U. dom O -> ( x C_ ( O ` y ) <-> x C_ ( O ` U. dom O ) ) )
70	69	ifbid 3922	. . . . . . . . . 10 |- ( y = U. dom O -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` U. dom O ) , ( F ` x ) , (/) ) )
71	70	mpteq2dv 4490	. . . . . . . . 9 |- ( 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 ) , (/) ) ) )
72	71	fveq2d 5806	. . . . . . . 8 |- ( 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 ) , (/) ) ) ) )
73		suceq 4895	. . . . . . . . 9 |- ( y = U. dom O -> suc y = suc U. dom O )
74	73	fveq2d 5806	. . . . . . . 8 |- ( y = U. dom O -> ( H ` suc y ) = ( H ` suc U. dom O ) )
75	72, 74	eleq12d 2536	. . . . . . 7 |- ( 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 ) ) )
76	67, 75	imbi12d 320	. . . . . 6 |- ( 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 ) ) ) )
77	76	imbi2d 316	. . . . 5 |- ( 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 ) ) ) ) )
78		eleq1 2526	. . . . . . . 8 |- ( y = (/) -> ( y e. dom O <-> (/) e. dom O ) )
79		sseq2 3489	. . . . . . . 8 |- ( y = (/) -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ (/) ) )
80	78, 79	anbi12d 710	. . . . . . 7 |- ( y = (/) -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) ) )
81		fveq2 5802	. . . . . . . . . . . 12 |- ( y = (/) -> ( O ` y ) = ( O ` (/) ) )
82	81	sseq2d 3495	. . . . . . . . . . 11 |- ( y = (/) -> ( x C_ ( O ` y ) <-> x C_ ( O ` (/) ) ) )
83	82	ifbid 3922	. . . . . . . . . 10 |- ( y = (/) -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) )
84	83	mpteq2dv 4490	. . . . . . . . 9 |- ( y = (/) -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) )
85	84	fveq2d 5806	. . . . . . . 8 |- ( 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 ) , (/) ) ) ) )
86		suceq 4895	. . . . . . . . 9 |- ( y = (/) -> suc y = suc (/) )
87	86	fveq2d 5806	. . . . . . . 8 |- ( y = (/) -> ( H ` suc y ) = ( H ` suc (/) ) )
88	85, 87	eleq12d 2536	. . . . . . 7 |- ( 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 (/) ) ) )
89	80, 88	imbi12d 320	. . . . . 6 |- ( 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 (/) ) ) ) )
90		eleq1 2526	. . . . . . . 8 |- ( y = u -> ( y e. dom O <-> u e. dom O ) )
91		sseq2 3489	. . . . . . . 8 |- ( y = u -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ u ) )
92	90, 91	anbi12d 710	. . . . . . 7 |- ( y = u -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( u e. dom O /\ ( `' O ` X ) C_ u ) ) )
93		fveq2 5802	. . . . . . . . . . . 12 |- ( y = u -> ( O ` y ) = ( O ` u ) )
94	93	sseq2d 3495	. . . . . . . . . . 11 |- ( y = u -> ( x C_ ( O ` y ) <-> x C_ ( O ` u ) ) )
95	94	ifbid 3922	. . . . . . . . . 10 |- ( y = u -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) )
96	95	mpteq2dv 4490	. . . . . . . . 9 |- ( y = u -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) )
97	96	fveq2d 5806	. . . . . . . 8 |- ( 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 ) , (/) ) ) ) )
98		suceq 4895	. . . . . . . . 9 |- ( y = u -> suc y = suc u )
99	98	fveq2d 5806	. . . . . . . 8 |- ( y = u -> ( H ` suc y ) = ( H ` suc u ) )
100	97, 99	eleq12d 2536	. . . . . . 7 |- ( 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 ) ) )
101	92, 100	imbi12d 320	. . . . . 6 |- ( 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 ) ) ) )
102		eleq1 2526	. . . . . . . 8 |- ( y = suc u -> ( y e. dom O <-> suc u e. dom O ) )
103		sseq2 3489	. . . . . . . 8 |- ( y = suc u -> ( ( `' O ` X ) C_ y <-> ( `' O ` X ) C_ suc u ) )
104	102, 103	anbi12d 710	. . . . . . 7 |- ( y = suc u -> ( ( y e. dom O /\ ( `' O ` X ) C_ y ) <-> ( suc u e. dom O /\ ( `' O ` X ) C_ suc u ) ) )
105		fveq2 5802	. . . . . . . . . . . 12 |- ( y = suc u -> ( O ` y ) = ( O ` suc u ) )
106	105	sseq2d 3495	. . . . . . . . . . 11 |- ( y = suc u -> ( x C_ ( O ` y ) <-> x C_ ( O ` suc u ) ) )
107	106	ifbid 3922	. . . . . . . . . 10 |- ( y = suc u -> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) )
108	107	mpteq2dv 4490	. . . . . . . . 9 |- ( y = suc u -> ( x e. B |-> if ( x C_ ( O ` y ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) )
109	108	fveq2d 5806	. . . . . . . 8 |- ( 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 ) , (/) ) ) ) )
110		suceq 4895	. . . . . . . . 9 |- ( y = suc u -> suc y = suc suc u )
111	110	fveq2d 5806	. . . . . . . 8 |- ( y = suc u -> ( H ` suc y ) = ( H ` suc suc u ) )
112	109, 111	eleq12d 2536	. . . . . . 7 |- ( 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 ) ) )
113	104, 112	imbi12d 320	. . . . . 6 |- ( 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 ) ) ) )
114		f1ocnvfv2 6096	. . . . . . . . . . . . 13 |- ( ( O : dom O -1-1-onto-> ( G supp (/) ) /\ X e. ( G supp (/) ) ) -> ( O ` ( `' O ` X ) ) = X )
115	55, 16, 114	syl2anc 661	. . . . . . . . . . . 12 |- ( ph -> ( O ` ( `' O ` X ) ) = X )
116	115	sseq2d 3495	. . . . . . . . . . 11 |- ( ph -> ( x C_ ( O ` ( `' O ` X ) ) <-> x C_ X ) )
117	116	ifbid 3922	. . . . . . . . . 10 |- ( ph -> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) = if ( x C_ X , ( F ` x ) , (/) ) )
118	117	mpteq2dv 4490	. . . . . . . . 9 |- ( ph -> ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) )
119	118	fveq2d 5806	. . . . . . . 8 |- ( 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 ) , (/) ) ) ) )
120		cantnflem1.h	. . . . . . . . 9 |- H = seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( G ` ( O ` k ) ) ) +o z ) ) , (/) )
121	8, 9, 10, 11, 12, 13, 14, 15, 2, 120	cantnflem1d 8010	. . . . . . . 8 |- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) )
122	119, 121	eqeltrd 2542	. . . . . . 7 |- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) )
123		ss0 3779	. . . . . . . . . . . . . 14 |- ( ( `' O ` X ) C_ (/) -> ( `' O ` X ) = (/) )
124	123	fveq2d 5806	. . . . . . . . . . . . 13 |- ( ( `' O ` X ) C_ (/) -> ( O ` ( `' O ` X ) ) = ( O ` (/) ) )
125	124	sseq2d 3495	. . . . . . . . . . . 12 |- ( ( `' O ` X ) C_ (/) -> ( x C_ ( O ` ( `' O ` X ) ) <-> x C_ ( O ` (/) ) ) )
126	125	ifbid 3922	. . . . . . . . . . 11 |- ( ( `' O ` X ) C_ (/) -> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) )
127	126	mpteq2dv 4490	. . . . . . . . . 10 |- ( ( `' O ` X ) C_ (/) -> ( x e. B |-> if ( x C_ ( O ` ( `' O ` X ) ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) )
128	127	fveq2d 5806	. . . . . . . . 9 |- ( ( `' 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 ) , (/) ) ) ) )
129		suceq 4895	. . . . . . . . . . 11 |- ( ( `' O ` X ) = (/) -> suc ( `' O ` X ) = suc (/) )
130	123, 129	syl 16	. . . . . . . . . 10 |- ( ( `' O ` X ) C_ (/) -> suc ( `' O ` X ) = suc (/) )
131	130	fveq2d 5806	. . . . . . . . 9 |- ( ( `' O ` X ) C_ (/) -> ( H ` suc ( `' O ` X ) ) = ( H ` suc (/) ) )
132	128, 131	eleq12d 2536	. . . . . . . 8 |- ( ( `' 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 (/) ) ) )
133	132	adantl 466	. . . . . . 7 |- ( ( (/) 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 (/) ) ) )
134	122, 133	syl5ibcom 220	. . . . . 6 |- ( ph -> ( ( (/) e. dom O /\ ( `' O ` X ) C_ (/) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` (/) ) , ( F ` x ) , (/) ) ) ) e. ( H ` suc (/) ) ) )
135		ordelon 4854	. . . . . . . . . . . . 13 |- ( ( Ord dom O /\ ( `' O ` X ) e. dom O ) -> ( `' O ` X ) e. On )
136	43, 59, 135	sylancr 663	. . . . . . . . . . . 12 |- ( ph -> ( `' O ` X ) e. On )
137	136	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ suc u e. dom O ) -> ( `' O ` X ) e. On )
138	43	a1i 11	. . . . . . . . . . . 12 |- ( ph -> Ord dom O )
139		ordelon 4854	. . . . . . . . . . . 12 |- ( ( Ord dom O /\ suc u e. dom O ) -> suc u e. On )
140	138, 139	sylan 471	. . . . . . . . . . 11 |- ( ( ph /\ suc u e. dom O ) -> suc u e. On )
141		onsseleq 4871	. . . . . . . . . . 11 |- ( ( ( `' O ` X ) e. On /\ suc u e. On ) -> ( ( `' O ` X ) C_ suc u <-> ( ( `' O ` X ) e. suc u \/ ( `' O ` X ) = suc u ) ) )
142	137, 140, 141	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ suc u <-> ( ( `' O ` X ) e. suc u \/ ( `' O ` X ) = suc u ) ) )
143		sucelon 6541	. . . . . . . . . . . . . . 15 |- ( u e. On <-> suc u e. On )
144	140, 143	sylibr 212	. . . . . . . . . . . . . 14 |- ( ( ph /\ suc u e. dom O ) -> u e. On )
145		eloni 4840	. . . . . . . . . . . . . 14 |- ( u e. On -> Ord u )
146	144, 145	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ suc u e. dom O ) -> Ord u )
147		ordsssuc 4916	. . . . . . . . . . . . 13 |- ( ( ( `' O ` X ) e. On /\ Ord u ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) )
148	137, 146, 147	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ suc u e. dom O ) -> ( ( `' O ` X ) C_ u <-> ( `' O ` X ) e. suc u ) )
149		ordtr 4844	. . . . . . . . . . . . . . . . 17 |- ( Ord dom O -> Tr dom O )
150	43, 149	mp1i 12	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> Tr dom O )
151		simprl 755	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc u e. dom O )
152		trsuc 4914	. . . . . . . . . . . . . . . 16 |- ( ( Tr dom O /\ suc u e. dom O ) -> u e. dom O )
153	150, 151, 152	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> u e. dom O )
154		simprr 756	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( `' O ` X ) C_ u )
155	153, 154	jca 532	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u e. dom O /\ ( `' O ` X ) C_ u ) )
156	9	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> A e. On )
157	10	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> B e. On )
158		oecl 7090	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
159	156, 157, 158	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A ^o B ) e. On )
160	8, 156, 157	cantnff 7996	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A CNF B ) : S --> ( A ^o B ) )
161	8, 9, 10	cantnfs 7988	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )
162	12, 161	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( F : B --> A /\ F finSupp (/) ) )
163	162	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> F : B --> A )
164	163	ffvelrnda 5955	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. B ) -> ( F ` x ) e. A )
165	8, 9, 10, 11, 12, 13, 14, 15	oemapvali 8006	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) )
166	165	simp1d 1000	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> X e. B )
167	22, 166	ffvelrnd 5956	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( G ` X ) e. A )
168		ne0i 3754	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( G ` X ) e. A -> A =/= (/) )
169	167, 168	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> A =/= (/) )
170		on0eln0 4885	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
171	9, 170	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( (/) e. A <-> A =/= (/) ) )
172	169, 171	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> (/) e. A )
173	172	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. B ) -> (/) e. A )
174	164, 173	ifcld 3943	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. B ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. A )
175		eqid 2454	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) )
176	174, 175	fmptd 5979	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) : B --> A )
177		mptexg 6059	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( B e. On -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. _V )
178	10, 177	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. _V )
179		funmpt 5565	. . . . . . . . . . . . . . . . . . . . . . 23 |- Fun ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) )
180	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> Fun ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) )
181	162	simprd 463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> F finSupp (/) )
182		eqid 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( F supp (/) ) = ( F supp (/) )
183		eqimss2 3520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( F supp (/) ) = ( F supp (/) ) -> ( F supp (/) ) C_ ( F supp (/) ) )
184	182, 183	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( F supp (/) ) C_ ( F supp (/) ) )
185		0ex 4533	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (/) e. _V
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> (/) e. _V )
187	163, 184, 10, 186	suppssr 6833	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ x e. ( B \ ( F supp (/) ) ) ) -> ( F ` x ) = (/) )
188	187	ifeq1d 3918	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ x e. ( B \ ( F supp (/) ) ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , (/) , (/) ) )
189		ifid 3937	. . . . . . . . . . . . . . . . . . . . . . . 24 |- if ( x C_ ( O ` u ) , (/) , (/) ) = (/)
190	188, 189	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. ( B \ ( F supp (/) ) ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = (/) )
191	190, 10	suppss2 6836	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) C_ ( F supp (/) ) )
192		fsuppsssupp 7750	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. _V /\ Fun ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) /\ ( F finSupp (/) /\ ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) C_ ( F supp (/) ) ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) finSupp (/) )
193	178, 180, 181, 191, 192	syl22anc 1220	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) finSupp (/) )
194	8, 9, 10	cantnfs 7988	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) , (/) ) ) finSupp (/) ) ) )
195	176, 193, 194	mpbir2and 913	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S )
196	195	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) e. S )
197	160, 196	ffvelrnd 5956	. . . . . . . . . . . . . . . . . 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. ( A ^o B ) )
198		onelon 4855	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 )
199	159, 197, 198	syl2anc 661	. . . . . . . . . . . . . . . . 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. On )
200	38	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> dom O e. om )
201		elnn 6599	. . . . . . . . . . . . . . . . . . 19 |- ( ( suc u e. dom O /\ dom O e. om ) -> suc u e. om )
202	151, 200, 201	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc u e. om )
203	120	cantnfvalf 7987	. . . . . . . . . . . . . . . . . . 19 |- H : om --> On
204	203	ffvelrni 5954	. . . . . . . . . . . . . . . . . 18 |- ( suc u e. om -> ( H ` suc u ) e. On )
205	202, 204	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( H ` suc u ) e. On )
206	25	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( G supp (/) ) C_ B )
207	2	oif 7858	. . . . . . . . . . . . . . . . . . . . . . 23 |- O : dom O --> ( G supp (/) )
208	207	ffvelrni 5954	. . . . . . . . . . . . . . . . . . . . . 22 |- ( suc u e. dom O -> ( O ` suc u ) e. ( G supp (/) ) )
209	151, 208	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. ( G supp (/) ) )
210	206, 209	sseldd 3468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. B )
211		onelon 4855	. . . . . . . . . . . . . . . . . . . 20 |- ( ( B e. On /\ ( O ` suc u ) e. B ) -> ( O ` suc u ) e. On )
212	157, 210, 211	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` suc u ) e. On )
213		oecl 7090	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. On /\ ( O ` suc u ) e. On ) -> ( A ^o ( O ` suc u ) ) e. On )
214	156, 212, 213	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( A ^o ( O ` suc u ) ) e. On )
215	163	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> F : B --> A )
216	215, 210	ffvelrnd 5956	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( F ` ( O ` suc u ) ) e. A )
217		onelon 4855	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. On /\ ( F ` ( O ` suc u ) ) e. A ) -> ( F ` ( O ` suc u ) ) e. On )
218	156, 216, 217	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( F ` ( O ` suc u ) ) e. On )
219		omcl 7089	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 )
220	214, 218, 219	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) e. On )
221		oaord 7099	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) ) ) )
222	199, 205, 220, 221	syl3anc 1219	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) )
223		ifeq1 3906	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F ` x ) = (/) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` suc u ) , (/) , (/) ) )
224		ifid 3937	. . . . . . . . . . . . . . . . . . . . . . 23 |- if ( x C_ ( O ` suc u ) , (/) , (/) ) = (/)
225	223, 224	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( F ` x ) = (/) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = (/) )
226		ifeq1 3906	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F ` x ) = (/) -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , (/) , (/) ) )
227		ifid 3937	. . . . . . . . . . . . . . . . . . . . . . 23 |- if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , (/) , (/) ) = (/)
228	226, 227	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( F ` x ) = (/) -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = (/) )
229	225, 228	eqeq12d 2476	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( F ` x ) = (/) -> ( if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) <-> (/) = (/) ) )
230		onss 6515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( B e. On -> B C_ On )
231	10, 230	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> B C_ On )
232	231	sselda 3467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ x e. B ) -> x e. On )
233	232	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> x e. On )
234	212	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( O ` suc u ) e. On )
235		onsseleq 4871	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( x e. On /\ ( O ` suc u ) e. On ) -> ( x C_ ( O ` suc u ) <-> ( x e. ( O ` suc u ) \/ x = ( O ` suc u ) ) ) )
236	233, 234, 235	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 ) ) ) )
237	236	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) ) )
238	233	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> x e. On )
239	207	ffvelrni 5954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u e. dom O -> ( O ` u ) e. ( G supp (/) ) )
240	153, 239	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. ( G supp (/) ) )
241	206, 240	sseldd 3468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. B )
242		onelon 4855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( B e. On /\ ( O ` u ) e. B ) -> ( O ` u ) e. On )
243	157, 241, 242	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. On )
244	243	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( O ` u ) e. On )
245		onsssuc 4917	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( x e. On /\ ( O ` u ) e. On ) -> ( x C_ ( O ` u ) <-> x e. suc ( O ` u ) ) )
246	238, 244, 245	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> x e. suc ( O ` u ) ) )
247		vex 3081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- u e. _V
248	247	sucid 4909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- u e. suc u
249	53	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
250		isorel 6129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( u e. dom O /\ suc u e. dom O ) ) -> ( u _E suc u <-> ( O ` u ) _E ( O ` suc u ) ) )
251	249, 153, 151, 250	syl12anc 1217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u _E suc u <-> ( O ` u ) _E ( O ` suc u ) ) )
252	247	sucex 6535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- suc u e. _V
253	252	epelc 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( u _E suc u <-> u e. suc u )
254		fvex 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( O ` suc u ) e. _V
255	254	epelc 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( O ` u ) _E ( O ` suc u ) <-> ( O ` u ) e. ( O ` suc u ) )
256	251, 253, 255	3bitr3g 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( u e. suc u <-> ( O ` u ) e. ( O ` suc u ) ) )
257	248, 256	mpbii 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( O ` u ) e. ( O ` suc u ) )
258		eloni 4840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( O ` suc u ) e. On -> Ord ( O ` suc u ) )
259	212, 258	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> Ord ( O ` suc u ) )
260		ordelsuc 6544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( O ` u ) e. On /\ Ord ( O ` suc u ) ) -> ( ( O ` u ) e. ( O ` suc u ) <-> suc ( O ` u ) C_ ( O ` suc u ) ) )
261	243, 259, 260	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( O ` u ) e. ( O ` suc u ) <-> suc ( O ` u ) C_ ( O ` suc u ) ) )
262	257, 261	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> suc ( O ` u ) C_ ( O ` suc u ) )
263	262	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> suc ( O ` u ) C_ ( O ` suc u ) )
264	263	sseld 3466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( 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 ) ) )
265	246, 264	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
266		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` u ) e. x )
267	249	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( 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 supp (/) ) ) )
268	267, 54	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( 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 supp (/) ) )
269	8, 9, 10, 11, 12, 13, 14, 15, 2	cantnflem1c 8009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> x e. ( G supp (/) ) )
270		f1ocnvfv2 6096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( O : dom O -1-1-onto-> ( G supp (/) ) /\ x e. ( G supp (/) ) ) -> ( O ` ( `' O ` x ) ) = x )
271	268, 269, 270	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( O ` ( `' O ` x ) ) = x )
272	266, 271	eleqtrrd 2545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( 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 ) ) )
273	153	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> u e. dom O )
274	268, 56, 57	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> `' O : ( G supp (/) ) --> dom O )
275	274, 269	ffvelrnd 5956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( `' O ` x ) e. dom O )
276		isorel 6129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( u e. dom O /\ ( `' O ` x ) e. dom O ) ) -> ( u _E ( `' O ` x ) <-> ( O ` u ) _E ( O ` ( `' O ` x ) ) ) )
277	267, 273, 275, 276	syl12anc 1217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
278		fvex 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( `' O ` x ) e. _V
279	278	epelc 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( u _E ( `' O ` x ) <-> u e. ( `' O ` x ) )
280		fvex 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( O ` ( `' O ` x ) ) e. _V
281	280	epelc 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( O ` u ) _E ( O ` ( `' O ` x ) ) <-> ( O ` u ) e. ( O ` ( `' O ` x ) ) )
282	277, 279, 281	3bitr3g 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( 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 ) ) ) )
283	272, 282	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> u e. ( `' O ` x ) )
284		ordelon 4854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( Ord dom O /\ ( `' O ` x ) e. dom O ) -> ( `' O ` x ) e. On )
285	43, 275, 284	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> ( `' O ` x ) e. On )
286		eloni 4840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( `' O ` x ) e. On -> Ord ( `' O ` x ) )
287	285, 286	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> Ord ( `' O ` x ) )
288		ordelsuc 6544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( u e. ( `' O ` x ) /\ Ord ( `' O ` x ) ) -> ( u e. ( `' O ` x ) <-> suc u C_ ( `' O ` x ) ) )
289	283, 287, 288	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( 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 ) ) )
290	283, 289	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u C_ ( `' O ` x ) )
291	151	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u e. dom O )
292	43, 291, 139	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> suc u e. On )
293		ontri1 4864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( suc u e. On /\ ( `' O ` x ) e. On ) -> ( suc u C_ ( `' O ` x ) <-> -. ( `' O ` x ) e. suc u ) )
294	292, 285, 293	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( 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 ) )
295	290, 294	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( ( F ` x ) =/= (/) /\ ( O ` u ) e. x ) ) -> -. ( `' O ` x ) e. suc u )
296		isorel 6129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( O Isom _E , _E ( dom O , ( G supp (/) ) ) /\ ( ( `' O ` x ) e. dom O /\ suc u e. dom O ) ) -> ( ( `' O ` x ) _E suc u <-> ( O ` ( `' O ` x ) ) _E ( O ` suc u ) ) )
297	267, 275, 291, 296	syl12anc 1217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
298	252	epelc 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( `' O ` x ) _E suc u <-> ( `' O ` x ) e. suc u )
299	254	epelc 4745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( O ` ( `' O ` x ) ) _E ( O ` suc u ) <-> ( O ` ( `' O ` x ) ) e. ( O ` suc u ) )
300	297, 298, 299	3bitr3g 287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 <-> ( O ` ( `' O ` x ) ) e. ( O ` suc u ) ) )
301	271	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( 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 ) ) )
302	300, 301	bitrd 253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( 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 ) ) )
303	295, 302	mtbid 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
304	303	expr 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( ( O ` u ) e. x -> -. x e. ( O ` suc u ) ) )
305	304	con2d 115	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. ( O ` suc u ) -> -. ( O ` u ) e. x ) )
306		ontri1 4864	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( x e. On /\ ( O ` u ) e. On ) -> ( x C_ ( O ` u ) <-> -. ( O ` u ) e. x ) )
307	238, 244, 306	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> -. ( O ` u ) e. x ) )
308	305, 307	sylibrd 234	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x e. ( O ` suc u ) -> x C_ ( O ` u ) ) )
309	265, 308	impbid 191	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> ( x C_ ( O ` u ) <-> x e. ( O ` suc u ) ) )
310	309	orbi1d 702	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) ) )
311	237, 310	bitr4d 256	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) ) ) )
312		orcom 387	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x C_ ( O ` u ) \/ x = ( O ` suc u ) ) <-> ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) )
313	311, 312	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) ) ) )
314	313	ifbid 3922	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) /\ ( F ` x ) =/= (/) ) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) )
315		eqidd 2455	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> (/) = (/) )
316	229, 314, 315	pm2.61ne 2767	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) = if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) )
317	316	mpteq2dva 4489	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) )
318	317	fveq2d 5806	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` suc u ) , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) ) )
319		fvex 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( F ` x ) e. _V
320	319, 185	ifex 3969	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V
321	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V )
322	321	ralrimivw 2831	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> A. x e. B if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V )
323	175	fnmpt 5648	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A. x e. B if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B )
324	322, 323	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B )
325	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> (/) e. _V )
326		suppvalfn 6810	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B /\ B e. On /\ (/) e. _V ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { y e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/) } )
327		nfcv 2616	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ y B
328		nfcv 2616	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ x B
329		nffvmpt1 5810	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- F/_ x ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y )
330		nfcv 2616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- F/_ x (/)
331	329, 330	nfne 2783	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/ x ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/)
332		nfv 1674	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/ y ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/)
333		fveq2 5802	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = x -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) = ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) )
334	333	neeq1d 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = x -> ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/) <-> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) ) )
335	327, 328, 331, 332, 334	cbvrab 3076	. . . . . . . . . . . . . . . . . . . . . . . 24 |- { y e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) =/= (/) } = { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) }
336	326, 335	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) Fn B /\ B e. On /\ (/) e. _V ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) } )
337	324, 157, 325, 336	syl3anc 1219	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) } )
338		eqidd 2455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) )
339	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V )
340	338, 339	fvmpt2d 5895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) = if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) )
341	340	neeq1d 2729	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) ) )
342	339	biantrurd 508	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) <-> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V /\ if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) ) ) )
343		dif1o 7053	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) <-> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. _V /\ if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) ) )
344	342, 343	syl6bbr 263	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) ) )
345	341, 344	bitrd 253	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) ) )
346	345	rabbidva 3069	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> { x e. B | ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` x ) =/= (/) } = { x e. B | if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) } )
347	337, 346	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) = { x e. B | if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) } )
348	320, 343	mpbiran 909	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) <-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) )
349		ifeq1 3906	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( F ` x ) = (/) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = if ( x C_ ( O ` u ) , (/) , (/) ) )
350	349, 189	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( F ` x ) = (/) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = (/) )
351	350	necon3i 2692	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> ( F ` x ) =/= (/) )
352		iffalse 3910	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( -. x C_ ( O ` u ) -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = (/) )
353	352	necon1ai 2683	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> x C_ ( O ` u ) )
354	351, 353	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> ( ( F ` x ) =/= (/) /\ x C_ ( O ` u ) ) )
355	265	expimpd 603	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( ( ( F ` x ) =/= (/) /\ x C_ ( O ` u ) ) -> x e. ( O ` suc u ) ) )
356	354, 355	syl5 32	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) =/= (/) -> x e. ( O ` suc u ) ) )
357	348, 356	syl5bi 217	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B ) -> ( if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) -> x e. ( O ` suc u ) ) )
358	357	3impia 1185	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) /\ x e. B /\ if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) ) -> x e. ( O ` suc u ) )
359	358	rabssdv 3543	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> { x e. B | if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) e. ( _V \ 1o ) } C_ ( O ` suc u ) )
360	347, 359	eqsstrd 3501	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) supp (/) ) C_ ( O ` suc u ) )
361		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = y -> ( x = ( O ` suc u ) <-> y = ( O ` suc u ) ) )
362		sseq1 3488	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = y -> ( x C_ ( O ` u ) <-> y C_ ( O ` u ) ) )
363	361, 362	orbi12d 709	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) <-> ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) ) )
364		fveq2 5802	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( F ` x ) = ( F ` y ) )
365	363, 364	ifbieq1d 3923	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) = if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) )
366	365	cbvmptv 4494	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) = ( y e. B |-> if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) )
367		fveq2 5802	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y = ( O ` suc u ) -> ( F ` y ) = ( F ` ( O ` suc u ) ) )
368	367	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( y e. B /\ y = ( O ` suc u ) ) -> ( F ` y ) = ( F ` ( O ` suc u ) ) )
369	368	ifeq1da 3930	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. B -> if ( y = ( O ` suc u ) , ( F ` y ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) )
370	362, 364	ifbieq1d 3923	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x = y -> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) = if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) )
371		fvex 5812	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( F ` y ) e. _V
372	371, 185	ifex 3969	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) e. _V
373	370, 175, 372	fvmpt 5886	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. B -> ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) = if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) )
374	373	ifeq2d 3919	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. B -> if ( y = ( O ` suc u ) , ( F ` y ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( y = ( O ` suc u ) , ( F ` y ) , if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) ) )
375		ifor 3947	. . . . . . . . . . . . . . . . . . . . . . . 24 |- if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) = if ( y = ( O ` suc u ) , ( F ` y ) , if ( y C_ ( O ` u ) , ( F ` y ) , (/) ) )
376	374, 375	syl6eqr 2513	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. B -> if ( y = ( O ` suc u ) , ( F ` y ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) )
377	369, 376	eqtr3d 2497	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. B -> if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) = if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) )
378	377	mpteq2ia 4485	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. B |-> if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) ) = ( y e. B |-> if ( ( y = ( O ` suc u ) \/ y C_ ( O ` u ) ) , ( F ` y ) , (/) ) )
379	366, 378	eqtr4i 2486	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) = ( y e. B |-> if ( y = ( O ` suc u ) , ( F ` ( O ` suc u ) ) , ( ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ` y ) ) )
380	8, 156, 157, 196, 210, 216, 360, 379	cantnfp1 8003	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( suc u e. dom O /\ ( `' O ` X ) C_ u ) ) -> ( ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) e. S /\ ( ( A CNF B ) ` ( x e. B |-> if ( ( x = ( O ` suc u ) \/ x C_ ( O ` u ) ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o ( O ` suc u ) ) .o ( F ` ( O ` suc u ) ) ) +o ( ( A CNF B ) ` ( x e. B |-> if ( x C_ ( O ` u ) , ( F ` x ) , (/) ) ) ) ) ) )
381	380	simprd 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( suc u