Theorem cantnfp1lem3 8577

Description: Lemma for cantnfp1 8578. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 1-Jul-2019.)

Hypotheses

Ref	Expression
cantnfs.s	|- S = dom ( A CNF B )
cantnfs.a	|- ( ph -> A e. On )
cantnfs.b	|- ( ph -> B e. On )
cantnfp1.g	|- ( ph -> G e. S )
cantnfp1.x	|- ( ph -> X e. B )
cantnfp1.y	|- ( ph -> Y e. A )
cantnfp1.s	|- ( ph -> ( G supp (/) ) C_ X )
cantnfp1.f	|- F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) )
cantnfp1.e	|- ( ph -> (/) e. Y )
cantnfp1.o	|- O = OrdIso ( _E , ( F supp (/) ) )
cantnfp1.h	|- H = seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( F ` ( O ` k ) ) ) +o z ) ) , (/) )
cantnfp1.k	|- K = OrdIso ( _E , ( G supp (/) ) )
cantnfp1.m	|- M = seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( K ` k ) ) .o ( G ` ( K ` k ) ) ) +o z ) ) , (/) )

Assertion

Ref	Expression
cantnfp1lem3	|- ( ph -> ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )

Distinct variable groups:   t, k, z, B   A, k, t, z   k, F, z   S, k, t, z   k, G, t, z   k, K, t, z   k, O, z   ph, k, t, z   k, Y, t, z   k, X, t, z

Allowed substitution hints:   F( t)   H( z, t, k)   M( z, t, k)   O( t)

Proof of Theorem cantnfp1lem3

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

Step	Hyp	Ref	Expression
1		cantnfs.s	. . 3 |- S = dom ( A CNF B )
2		cantnfs.a	. . 3 |- ( ph -> A e. On )
3		cantnfs.b	. . 3 |- ( ph -> B e. On )
4		cantnfp1.o	. . 3 |- O = OrdIso ( _E , ( F supp (/) ) )
5		cantnfp1.g	. . . 4 |- ( ph -> G e. S )
6		cantnfp1.x	. . . 4 |- ( ph -> X e. B )
7		cantnfp1.y	. . . 4 |- ( ph -> Y e. A )
8		cantnfp1.s	. . . 4 |- ( ph -> ( G supp (/) ) C_ X )
9		cantnfp1.f	. . . 4 |- F = ( t e. B |-> if ( t = X , Y , ( G ` t ) ) )
10	1, 2, 3, 5, 6, 7, 8, 9	cantnfp1lem1 8575	. . 3 |- ( ph -> F e. S )
11		cantnfp1.h	. . 3 |- H = seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( F ` ( O ` k ) ) ) +o z ) ) , (/) )
12	1, 2, 3, 4, 10, 11	cantnfval 8565	. 2 |- ( ph -> ( ( A CNF B ) ` F ) = ( H ` dom O ) )
13		cantnfp1.e	. . . 4 |- ( ph -> (/) e. Y )
14	1, 2, 3, 5, 6, 7, 8, 9, 13, 4	cantnfp1lem2 8576	. . 3 |- ( ph -> dom O = suc U. dom O )
15	14	fveq2d 6195	. 2 |- ( ph -> ( H ` dom O ) = ( H ` suc U. dom O ) )
16	1, 2, 3, 4, 10	cantnfcl 8564	. . . . . . 7 |- ( ph -> ( _E We ( F supp (/) ) /\ dom O e. om ) )
17	16	simprd 479	. . . . . 6 |- ( ph -> dom O e. om )
18	14, 17	eqeltrrd 2702	. . . . 5 |- ( ph -> suc U. dom O e. om )
19		peano2b 7081	. . . . 5 |- ( U. dom O e. om <-> suc U. dom O e. om )
20	18, 19	sylibr 224	. . . 4 |- ( ph -> U. dom O e. om )
21	1, 2, 3, 4, 10, 11	cantnfsuc 8567	. . . 4 |- ( ( ph /\ U. dom O e. om ) -> ( H ` suc U. dom O ) = ( ( ( A ^o ( O ` U. dom O ) ) .o ( F ` ( O ` U. dom O ) ) ) +o ( H ` U. dom O ) ) )
22	20, 21	mpdan 702	. . 3 |- ( ph -> ( H ` suc U. dom O ) = ( ( ( A ^o ( O ` U. dom O ) ) .o ( F ` ( O ` U. dom O ) ) ) +o ( H ` U. dom O ) ) )
23		suppssdm 7308	. . . . . . . . . . . . . . . . 17 |- ( F supp (/) ) C_ dom F
24	7	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ t e. B ) -> Y e. A )
25	1, 2, 3	cantnfs 8563	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
26	5, 25	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( G : B --> A /\ G finSupp (/) ) )
27	26	simpld 475	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> G : B --> A )
28	27	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ t e. B ) -> ( G ` t ) e. A )
29	24, 28	ifcld 4131	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ t e. B ) -> if ( t = X , Y , ( G ` t ) ) e. A )
30	29, 9	fmptd 6385	. . . . . . . . . . . . . . . . . 18 |- ( ph -> F : B --> A )
31		fdm 6051	. . . . . . . . . . . . . . . . . 18 |- ( F : B --> A -> dom F = B )
32	30, 31	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom F = B )
33	23, 32	syl5sseq 3653	. . . . . . . . . . . . . . . 16 |- ( ph -> ( F supp (/) ) C_ B )
34	3, 33	ssexd 4805	. . . . . . . . . . . . . . 15 |- ( ph -> ( F supp (/) ) e. _V )
35	16	simpld 475	. . . . . . . . . . . . . . 15 |- ( ph -> _E We ( F supp (/) ) )
36	4	oiiso 8442	. . . . . . . . . . . . . . 15 |- ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> O Isom _E , _E ( dom O , ( F supp (/) ) ) )
37	34, 35, 36	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ph -> O Isom _E , _E ( dom O , ( F supp (/) ) ) )
38		isof1o 6573	. . . . . . . . . . . . . 14 |- ( O Isom _E , _E ( dom O , ( F supp (/) ) ) -> O : dom O -1-1-onto-> ( F supp (/) ) )
39	37, 38	syl 17	. . . . . . . . . . . . 13 |- ( ph -> O : dom O -1-1-onto-> ( F supp (/) ) )
40		f1ocnv 6149	. . . . . . . . . . . . 13 |- ( O : dom O -1-1-onto-> ( F supp (/) ) -> `' O : ( F supp (/) ) -1-1-onto-> dom O )
41		f1of 6137	. . . . . . . . . . . . 13 |- ( `' O : ( F supp (/) ) -1-1-onto-> dom O -> `' O : ( F supp (/) ) --> dom O )
42	39, 40, 41	3syl 18	. . . . . . . . . . . 12 |- ( ph -> `' O : ( F supp (/) ) --> dom O )
43		iftrue 4092	. . . . . . . . . . . . . . . 16 |- ( t = X -> if ( t = X , Y , ( G ` t ) ) = Y )
44	43, 9	fvmptg 6280	. . . . . . . . . . . . . . 15 |- ( ( X e. B /\ Y e. A ) -> ( F ` X ) = Y )
45	6, 7, 44	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ph -> ( F ` X ) = Y )
46		onelon 5748	. . . . . . . . . . . . . . . . 17 |- ( ( A e. On /\ Y e. A ) -> Y e. On )
47	2, 7, 46	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ph -> Y e. On )
48		on0eln0 5780	. . . . . . . . . . . . . . . 16 |- ( Y e. On -> ( (/) e. Y <-> Y =/= (/) ) )
49	47, 48	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> ( (/) e. Y <-> Y =/= (/) ) )
50	13, 49	mpbid 222	. . . . . . . . . . . . . 14 |- ( ph -> Y =/= (/) )
51	45, 50	eqnetrd 2861	. . . . . . . . . . . . 13 |- ( ph -> ( F ` X ) =/= (/) )
52		ffn 6045	. . . . . . . . . . . . . . 15 |- ( F : B --> A -> F Fn B )
53	30, 52	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> F Fn B )
54		0ex 4790	. . . . . . . . . . . . . . 15 |- (/) e. _V
55	54	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> (/) e. _V )
56		elsuppfn 7303	. . . . . . . . . . . . . 14 |- ( ( F Fn B /\ B e. On /\ (/) e. _V ) -> ( X e. ( F supp (/) ) <-> ( X e. B /\ ( F ` X ) =/= (/) ) ) )
57	53, 3, 55, 56	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ph -> ( X e. ( F supp (/) ) <-> ( X e. B /\ ( F ` X ) =/= (/) ) ) )
58	6, 51, 57	mpbir2and 957	. . . . . . . . . . . 12 |- ( ph -> X e. ( F supp (/) ) )
59	42, 58	ffvelrnd 6360	. . . . . . . . . . 11 |- ( ph -> ( `' O ` X ) e. dom O )
60		elssuni 4467	. . . . . . . . . . 11 |- ( ( `' O ` X ) e. dom O -> ( `' O ` X ) C_ U. dom O )
61	59, 60	syl 17	. . . . . . . . . 10 |- ( ph -> ( `' O ` X ) C_ U. dom O )
62	4	oicl 8434	. . . . . . . . . . . 12 |- Ord dom O
63		ordelon 5747	. . . . . . . . . . . 12 |- ( ( Ord dom O /\ ( `' O ` X ) e. dom O ) -> ( `' O ` X ) e. On )
64	62, 59, 63	sylancr 695	. . . . . . . . . . 11 |- ( ph -> ( `' O ` X ) e. On )
65		nnon 7071	. . . . . . . . . . . 12 |- ( U. dom O e. om -> U. dom O e. On )
66	20, 65	syl 17	. . . . . . . . . . 11 |- ( ph -> U. dom O e. On )
67		ontri1 5757	. . . . . . . . . . 11 |- ( ( ( `' O ` X ) e. On /\ U. dom O e. On ) -> ( ( `' O ` X ) C_ U. dom O <-> -. U. dom O e. ( `' O ` X ) ) )
68	64, 66, 67	syl2anc 693	. . . . . . . . . 10 |- ( ph -> ( ( `' O ` X ) C_ U. dom O <-> -. U. dom O e. ( `' O ` X ) ) )
69	61, 68	mpbid 222	. . . . . . . . 9 |- ( ph -> -. U. dom O e. ( `' O ` X ) )
70		sucidg 5803	. . . . . . . . . . . . . 14 |- ( U. dom O e. om -> U. dom O e. suc U. dom O )
71	20, 70	syl 17	. . . . . . . . . . . . 13 |- ( ph -> U. dom O e. suc U. dom O )
72	71, 14	eleqtrrd 2704	. . . . . . . . . . . 12 |- ( ph -> U. dom O e. dom O )
73		isorel 6576	. . . . . . . . . . . 12 |- ( ( O Isom _E , _E ( dom O , ( F supp (/) ) ) /\ ( 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 ) ) ) )
74	37, 72, 59, 73	syl12anc 1324	. . . . . . . . . . 11 |- ( ph -> ( U. dom O _E ( `' O ` X ) <-> ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) ) )
75		fvex 6201	. . . . . . . . . . . 12 |- ( `' O ` X ) e. _V
76	75	epelc 5031	. . . . . . . . . . 11 |- ( U. dom O _E ( `' O ` X ) <-> U. dom O e. ( `' O ` X ) )
77		fvex 6201	. . . . . . . . . . . 12 |- ( O ` ( `' O ` X ) ) e. _V
78	77	epelc 5031	. . . . . . . . . . 11 |- ( ( O ` U. dom O ) _E ( O ` ( `' O ` X ) ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) )
79	74, 76, 78	3bitr3g 302	. . . . . . . . . 10 |- ( ph -> ( U. dom O e. ( `' O ` X ) <-> ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) ) )
80		f1ocnvfv2 6533	. . . . . . . . . . . 12 |- ( ( O : dom O -1-1-onto-> ( F supp (/) ) /\ X e. ( F supp (/) ) ) -> ( O ` ( `' O ` X ) ) = X )
81	39, 58, 80	syl2anc 693	. . . . . . . . . . 11 |- ( ph -> ( O ` ( `' O ` X ) ) = X )
82	81	eleq2d 2687	. . . . . . . . . 10 |- ( ph -> ( ( O ` U. dom O ) e. ( O ` ( `' O ` X ) ) <-> ( O ` U. dom O ) e. X ) )
83	79, 82	bitrd 268	. . . . . . . . 9 |- ( ph -> ( U. dom O e. ( `' O ` X ) <-> ( O ` U. dom O ) e. X ) )
84	69, 83	mtbid 314	. . . . . . . 8 |- ( ph -> -. ( O ` U. dom O ) e. X )
85	8	sseld 3602	. . . . . . . . . 10 |- ( ph -> ( ( O ` U. dom O ) e. ( G supp (/) ) -> ( O ` U. dom O ) e. X ) )
86		onss 6990	. . . . . . . . . . . . . . . 16 |- ( B e. On -> B C_ On )
87	3, 86	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> B C_ On )
88	33, 87	sstrd 3613	. . . . . . . . . . . . . 14 |- ( ph -> ( F supp (/) ) C_ On )
89	4	oif 8435	. . . . . . . . . . . . . . . 16 |- O : dom O --> ( F supp (/) )
90	89	ffvelrni 6358	. . . . . . . . . . . . . . 15 |- ( U. dom O e. dom O -> ( O ` U. dom O ) e. ( F supp (/) ) )
91	72, 90	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( O ` U. dom O ) e. ( F supp (/) ) )
92	88, 91	sseldd 3604	. . . . . . . . . . . . 13 |- ( ph -> ( O ` U. dom O ) e. On )
93		eloni 5733	. . . . . . . . . . . . 13 |- ( ( O ` U. dom O ) e. On -> Ord ( O ` U. dom O ) )
94	92, 93	syl 17	. . . . . . . . . . . 12 |- ( ph -> Ord ( O ` U. dom O ) )
95		ordn2lp 5743	. . . . . . . . . . . 12 |- ( Ord ( O ` U. dom O ) -> -. ( ( O ` U. dom O ) e. X /\ X e. ( O ` U. dom O ) ) )
96	94, 95	syl 17	. . . . . . . . . . 11 |- ( ph -> -. ( ( O ` U. dom O ) e. X /\ X e. ( O ` U. dom O ) ) )
97		imnan 438	. . . . . . . . . . 11 |- ( ( ( O ` U. dom O ) e. X -> -. X e. ( O ` U. dom O ) ) <-> -. ( ( O ` U. dom O ) e. X /\ X e. ( O ` U. dom O ) ) )
98	96, 97	sylibr 224	. . . . . . . . . 10 |- ( ph -> ( ( O ` U. dom O ) e. X -> -. X e. ( O ` U. dom O ) ) )
99	85, 98	syld 47	. . . . . . . . 9 |- ( ph -> ( ( O ` U. dom O ) e. ( G supp (/) ) -> -. X e. ( O ` U. dom O ) ) )
100		onelon 5748	. . . . . . . . . . . . 13 |- ( ( B e. On /\ X e. B ) -> X e. On )
101	3, 6, 100	syl2anc 693	. . . . . . . . . . . 12 |- ( ph -> X e. On )
102		eloni 5733	. . . . . . . . . . . 12 |- ( X e. On -> Ord X )
103	101, 102	syl 17	. . . . . . . . . . 11 |- ( ph -> Ord X )
104		ordirr 5741	. . . . . . . . . . 11 |- ( Ord X -> -. X e. X )
105	103, 104	syl 17	. . . . . . . . . 10 |- ( ph -> -. X e. X )
106		elsni 4194	. . . . . . . . . . . 12 |- ( ( O ` U. dom O ) e. { X } -> ( O ` U. dom O ) = X )
107	106	eleq2d 2687	. . . . . . . . . . 11 |- ( ( O ` U. dom O ) e. { X } -> ( X e. ( O ` U. dom O ) <-> X e. X ) )
108	107	notbid 308	. . . . . . . . . 10 |- ( ( O ` U. dom O ) e. { X } -> ( -. X e. ( O ` U. dom O ) <-> -. X e. X ) )
109	105, 108	syl5ibrcom 237	. . . . . . . . 9 |- ( ph -> ( ( O ` U. dom O ) e. { X } -> -. X e. ( O ` U. dom O ) ) )
110		eldifi 3732	. . . . . . . . . . . . . . 15 |- ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> k e. B )
111	110	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> k e. B )
112	7	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> Y e. A )
113		fvex 6201	. . . . . . . . . . . . . . 15 |- ( G ` k ) e. _V
114		ifexg 4157	. . . . . . . . . . . . . . 15 |- ( ( Y e. A /\ ( G ` k ) e. _V ) -> if ( k = X , Y , ( G ` k ) ) e. _V )
115	112, 113, 114	sylancl 694	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> if ( k = X , Y , ( G ` k ) ) e. _V )
116		eqeq1 2626	. . . . . . . . . . . . . . . 16 |- ( t = k -> ( t = X <-> k = X ) )
117		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( t = k -> ( G ` t ) = ( G ` k ) )
118	116, 117	ifbieq2d 4111	. . . . . . . . . . . . . . 15 |- ( t = k -> if ( t = X , Y , ( G ` t ) ) = if ( k = X , Y , ( G ` k ) ) )
119	118, 9	fvmptg 6280	. . . . . . . . . . . . . 14 |- ( ( k e. B /\ if ( k = X , Y , ( G ` k ) ) e. _V ) -> ( F ` k ) = if ( k = X , Y , ( G ` k ) ) )
120	111, 115, 119	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( F ` k ) = if ( k = X , Y , ( G ` k ) ) )
121		eldifn 3733	. . . . . . . . . . . . . . . 16 |- ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> -. k e. ( ( G supp (/) ) u. { X } ) )
122	121	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> -. k e. ( ( G supp (/) ) u. { X } ) )
123		velsn 4193	. . . . . . . . . . . . . . . 16 |- ( k e. { X } <-> k = X )
124		elun2 3781	. . . . . . . . . . . . . . . 16 |- ( k e. { X } -> k e. ( ( G supp (/) ) u. { X } ) )
125	123, 124	sylbir 225	. . . . . . . . . . . . . . 15 |- ( k = X -> k e. ( ( G supp (/) ) u. { X } ) )
126	122, 125	nsyl 135	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> -. k = X )
127	126	iffalsed 4097	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> if ( k = X , Y , ( G ` k ) ) = ( G ` k ) )
128		ssun1 3776	. . . . . . . . . . . . . . . 16 |- ( G supp (/) ) C_ ( ( G supp (/) ) u. { X } )
129		sscon 3744	. . . . . . . . . . . . . . . 16 |- ( ( G supp (/) ) C_ ( ( G supp (/) ) u. { X } ) -> ( B \ ( ( G supp (/) ) u. { X } ) ) C_ ( B \ ( G supp (/) ) ) )
130	128, 129	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( B \ ( ( G supp (/) ) u. { X } ) ) C_ ( B \ ( G supp (/) ) )
131	130	sseli 3599	. . . . . . . . . . . . . 14 |- ( k e. ( B \ ( ( G supp (/) ) u. { X } ) ) -> k e. ( B \ ( G supp (/) ) ) )
132		ssid 3624	. . . . . . . . . . . . . . . 16 |- ( G supp (/) ) C_ ( G supp (/) )
133	132	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> ( G supp (/) ) C_ ( G supp (/) ) )
134	27, 133, 3, 13	suppssr 7326	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( B \ ( G supp (/) ) ) ) -> ( G ` k ) = (/) )
135	131, 134	sylan2 491	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( G ` k ) = (/) )
136	120, 127, 135	3eqtrd 2660	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( B \ ( ( G supp (/) ) u. { X } ) ) ) -> ( F ` k ) = (/) )
137	30, 136	suppss 7325	. . . . . . . . . . 11 |- ( ph -> ( F supp (/) ) C_ ( ( G supp (/) ) u. { X } ) )
138	137, 91	sseldd 3604	. . . . . . . . . 10 |- ( ph -> ( O ` U. dom O ) e. ( ( G supp (/) ) u. { X } ) )
139		elun 3753	. . . . . . . . . 10 |- ( ( O ` U. dom O ) e. ( ( G supp (/) ) u. { X } ) <-> ( ( O ` U. dom O ) e. ( G supp (/) ) \/ ( O ` U. dom O ) e. { X } ) )
140	138, 139	sylib 208	. . . . . . . . 9 |- ( ph -> ( ( O ` U. dom O ) e. ( G supp (/) ) \/ ( O ` U. dom O ) e. { X } ) )
141	99, 109, 140	mpjaod 396	. . . . . . . 8 |- ( ph -> -. X e. ( O ` U. dom O ) )
142		ioran 511	. . . . . . . 8 |- ( -. ( ( O ` U. dom O ) e. X \/ X e. ( O ` U. dom O ) ) <-> ( -. ( O ` U. dom O ) e. X /\ -. X e. ( O ` U. dom O ) ) )
143	84, 141, 142	sylanbrc 698	. . . . . . 7 |- ( ph -> -. ( ( O ` U. dom O ) e. X \/ X e. ( O ` U. dom O ) ) )
144		ordtri3 5759	. . . . . . . 8 |- ( ( Ord ( O ` U. dom O ) /\ Ord X ) -> ( ( O ` U. dom O ) = X <-> -. ( ( O ` U. dom O ) e. X \/ X e. ( O ` U. dom O ) ) ) )
145	94, 103, 144	syl2anc 693	. . . . . . 7 |- ( ph -> ( ( O ` U. dom O ) = X <-> -. ( ( O ` U. dom O ) e. X \/ X e. ( O ` U. dom O ) ) ) )
146	143, 145	mpbird 247	. . . . . 6 |- ( ph -> ( O ` U. dom O ) = X )
147	146	oveq2d 6666	. . . . 5 |- ( ph -> ( A ^o ( O ` U. dom O ) ) = ( A ^o X ) )
148	146	fveq2d 6195	. . . . . 6 |- ( ph -> ( F ` ( O ` U. dom O ) ) = ( F ` X ) )
149	148, 45	eqtrd 2656	. . . . 5 |- ( ph -> ( F ` ( O ` U. dom O ) ) = Y )
150	147, 149	oveq12d 6668	. . . 4 |- ( ph -> ( ( A ^o ( O ` U. dom O ) ) .o ( F ` ( O ` U. dom O ) ) ) = ( ( A ^o X ) .o Y ) )
151		nnord 7073	. . . . . . . . 9 |- ( U. dom O e. om -> Ord U. dom O )
152	20, 151	syl 17	. . . . . . . 8 |- ( ph -> Ord U. dom O )
153		sssucid 5802	. . . . . . . . . 10 |- U. dom O C_ suc U. dom O
154	153, 14	syl5sseqr 3654	. . . . . . . . 9 |- ( ph -> U. dom O C_ dom O )
155		f1ofo 6144	. . . . . . . . . . . . 13 |- ( O : dom O -1-1-onto-> ( F supp (/) ) -> O : dom O -onto-> ( F supp (/) ) )
156	39, 155	syl 17	. . . . . . . . . . . 12 |- ( ph -> O : dom O -onto-> ( F supp (/) ) )
157		foima 6120	. . . . . . . . . . . 12 |- ( O : dom O -onto-> ( F supp (/) ) -> ( O " dom O ) = ( F supp (/) ) )
158	156, 157	syl 17	. . . . . . . . . . 11 |- ( ph -> ( O " dom O ) = ( F supp (/) ) )
159		ffn 6045	. . . . . . . . . . . . . 14 |- ( O : dom O --> ( F supp (/) ) -> O Fn dom O )
160	89, 159	ax-mp 5	. . . . . . . . . . . . 13 |- O Fn dom O
161		fnsnfv 6258	. . . . . . . . . . . . 13 |- ( ( O Fn dom O /\ U. dom O e. dom O ) -> { ( O ` U. dom O ) } = ( O " { U. dom O } ) )
162	160, 72, 161	sylancr 695	. . . . . . . . . . . 12 |- ( ph -> { ( O ` U. dom O ) } = ( O " { U. dom O } ) )
163	146	sneqd 4189	. . . . . . . . . . . 12 |- ( ph -> { ( O ` U. dom O ) } = { X } )
164	162, 163	eqtr3d 2658	. . . . . . . . . . 11 |- ( ph -> ( O " { U. dom O } ) = { X } )
165	158, 164	difeq12d 3729	. . . . . . . . . 10 |- ( ph -> ( ( O " dom O ) \ ( O " { U. dom O } ) ) = ( ( F supp (/) ) \ { X } ) )
166		ordirr 5741	. . . . . . . . . . . . . . . . 17 |- ( Ord U. dom O -> -. U. dom O e. U. dom O )
167	152, 166	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> -. U. dom O e. U. dom O )
168		disjsn 4246	. . . . . . . . . . . . . . . 16 |- ( ( U. dom O i^i { U. dom O } ) = (/) <-> -. U. dom O e. U. dom O )
169	167, 168	sylibr 224	. . . . . . . . . . . . . . 15 |- ( ph -> ( U. dom O i^i { U. dom O } ) = (/) )
170		disj3 4021	. . . . . . . . . . . . . . 15 |- ( ( U. dom O i^i { U. dom O } ) = (/) <-> U. dom O = ( U. dom O \ { U. dom O } ) )
171	169, 170	sylib 208	. . . . . . . . . . . . . 14 |- ( ph -> U. dom O = ( U. dom O \ { U. dom O } ) )
172		difun2 4048	. . . . . . . . . . . . . 14 |- ( ( U. dom O u. { U. dom O } ) \ { U. dom O } ) = ( U. dom O \ { U. dom O } )
173	171, 172	syl6eqr 2674	. . . . . . . . . . . . 13 |- ( ph -> U. dom O = ( ( U. dom O u. { U. dom O } ) \ { U. dom O } ) )
174		df-suc 5729	. . . . . . . . . . . . . . 15 |- suc U. dom O = ( U. dom O u. { U. dom O } )
175	14, 174	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( ph -> dom O = ( U. dom O u. { U. dom O } ) )
176	175	difeq1d 3727	. . . . . . . . . . . . 13 |- ( ph -> ( dom O \ { U. dom O } ) = ( ( U. dom O u. { U. dom O } ) \ { U. dom O } ) )
177	173, 176	eqtr4d 2659	. . . . . . . . . . . 12 |- ( ph -> U. dom O = ( dom O \ { U. dom O } ) )
178	177	imaeq2d 5466	. . . . . . . . . . 11 |- ( ph -> ( O " U. dom O ) = ( O " ( dom O \ { U. dom O } ) ) )
179		dff1o3 6143	. . . . . . . . . . . . 13 |- ( O : dom O -1-1-onto-> ( F supp (/) ) <-> ( O : dom O -onto-> ( F supp (/) ) /\ Fun `' O ) )
180	179	simprbi 480	. . . . . . . . . . . 12 |- ( O : dom O -1-1-onto-> ( F supp (/) ) -> Fun `' O )
181		imadif 5973	. . . . . . . . . . . 12 |- ( Fun `' O -> ( O " ( dom O \ { U. dom O } ) ) = ( ( O " dom O ) \ ( O " { U. dom O } ) ) )
182	39, 180, 181	3syl 18	. . . . . . . . . . 11 |- ( ph -> ( O " ( dom O \ { U. dom O } ) ) = ( ( O " dom O ) \ ( O " { U. dom O } ) ) )
183	178, 182	eqtrd 2656	. . . . . . . . . 10 |- ( ph -> ( O " U. dom O ) = ( ( O " dom O ) \ ( O " { U. dom O } ) ) )
184	8, 105	ssneldd 3606	. . . . . . . . . . . . 13 |- ( ph -> -. X e. ( G supp (/) ) )
185		disjsn 4246	. . . . . . . . . . . . 13 |- ( ( ( G supp (/) ) i^i { X } ) = (/) <-> -. X e. ( G supp (/) ) )
186	184, 185	sylibr 224	. . . . . . . . . . . 12 |- ( ph -> ( ( G supp (/) ) i^i { X } ) = (/) )
187		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21 |- ( G ` X ) e. _V
188		dif1o 7580	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( G ` X ) e. ( _V \ 1o ) <-> ( ( G ` X ) e. _V /\ ( G ` X ) =/= (/) ) )
189	187, 188	mpbiran 953	. . . . . . . . . . . . . . . . . . . 20 |- ( ( G ` X ) e. ( _V \ 1o ) <-> ( G ` X ) =/= (/) )
190		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( G : B --> A -> G Fn B )
191	27, 190	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> G Fn B )
192		elsuppfn 7303	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( G Fn B /\ B e. On /\ (/) e. _V ) -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
193	191, 3, 55, 192	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) =/= (/) ) ) )
194	189	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( G ` X ) e. ( _V \ 1o ) <-> ( G ` X ) =/= (/) ) )
195	194	bicomd 213	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( ( G ` X ) =/= (/) <-> ( G ` X ) e. ( _V \ 1o ) ) )
196	195	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( X e. B /\ ( G ` X ) =/= (/) ) <-> ( X e. B /\ ( G ` X ) e. ( _V \ 1o ) ) ) )
197	193, 196	bitrd 268	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( X e. ( G supp (/) ) <-> ( X e. B /\ ( G ` X ) e. ( _V \ 1o ) ) ) )
198	8	sseld 3602	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( X e. ( G supp (/) ) -> X e. X ) )
199	197, 198	sylbird 250	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( X e. B /\ ( G ` X ) e. ( _V \ 1o ) ) -> X e. X ) )
200	6, 199	mpand 711	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( G ` X ) e. ( _V \ 1o ) -> X e. X ) )
201	189, 200	syl5bir 233	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( G ` X ) =/= (/) -> X e. X ) )
202	201	necon1bd 2812	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( -. X e. X -> ( G ` X ) = (/) ) )
203	105, 202	mpd 15	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G ` X ) = (/) )
204	203	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( G ` X ) = (/) )
205		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( k = X -> ( G ` k ) = ( G ` X ) )
206	205	eqeq1d 2624	. . . . . . . . . . . . . . . 16 |- ( k = X -> ( ( G ` k ) = (/) <-> ( G ` X ) = (/) ) )
207	204, 206	syl5ibrcom 237	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( k = X -> ( G ` k ) = (/) ) )
208		eldifi 3732	. . . . . . . . . . . . . . . . . . 19 |- ( k e. ( B \ ( F supp (/) ) ) -> k e. B )
209	208	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> k e. B )
210	7	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> Y e. A )
211	210, 113, 114	sylancl 694	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> if ( k = X , Y , ( G ` k ) ) e. _V )
212	209, 211, 119	syl2anc 693	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( F ` k ) = if ( k = X , Y , ( G ` k ) ) )
213		ssid 3624	. . . . . . . . . . . . . . . . . . 19 |- ( F supp (/) ) C_ ( F supp (/) )
214	213	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( F supp (/) ) C_ ( F supp (/) ) )
215	30, 214, 3, 13	suppssr 7326	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( F ` k ) = (/) )
216	212, 215	eqtr3d 2658	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> if ( k = X , Y , ( G ` k ) ) = (/) )
217		iffalse 4095	. . . . . . . . . . . . . . . . 17 |- ( -. k = X -> if ( k = X , Y , ( G ` k ) ) = ( G ` k ) )
218	217	eqeq1d 2624	. . . . . . . . . . . . . . . 16 |- ( -. k = X -> ( if ( k = X , Y , ( G ` k ) ) = (/) <-> ( G ` k ) = (/) ) )
219	216, 218	syl5ibcom 235	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( -. k = X -> ( G ` k ) = (/) ) )
220	207, 219	pm2.61d 170	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( B \ ( F supp (/) ) ) ) -> ( G ` k ) = (/) )
221	27, 220	suppss 7325	. . . . . . . . . . . . 13 |- ( ph -> ( G supp (/) ) C_ ( F supp (/) ) )
222		reldisj 4020	. . . . . . . . . . . . 13 |- ( ( G supp (/) ) C_ ( F supp (/) ) -> ( ( ( G supp (/) ) i^i { X } ) = (/) <-> ( G supp (/) ) C_ ( ( F supp (/) ) \ { X } ) ) )
223	221, 222	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( ( ( G supp (/) ) i^i { X } ) = (/) <-> ( G supp (/) ) C_ ( ( F supp (/) ) \ { X } ) ) )
224	186, 223	mpbid 222	. . . . . . . . . . 11 |- ( ph -> ( G supp (/) ) C_ ( ( F supp (/) ) \ { X } ) )
225		uncom 3757	. . . . . . . . . . . . 13 |- ( ( G supp (/) ) u. { X } ) = ( { X } u. ( G supp (/) ) )
226	137, 225	syl6sseq 3651	. . . . . . . . . . . 12 |- ( ph -> ( F supp (/) ) C_ ( { X } u. ( G supp (/) ) ) )
227		ssundif 4052	. . . . . . . . . . . 12 |- ( ( F supp (/) ) C_ ( { X } u. ( G supp (/) ) ) <-> ( ( F supp (/) ) \ { X } ) C_ ( G supp (/) ) )
228	226, 227	sylib 208	. . . . . . . . . . 11 |- ( ph -> ( ( F supp (/) ) \ { X } ) C_ ( G supp (/) ) )
229	224, 228	eqssd 3620	. . . . . . . . . 10 |- ( ph -> ( G supp (/) ) = ( ( F supp (/) ) \ { X } ) )
230	165, 183, 229	3eqtr4rd 2667	. . . . . . . . 9 |- ( ph -> ( G supp (/) ) = ( O " U. dom O ) )
231		isores3 6585	. . . . . . . . 9 |- ( ( O Isom _E , _E ( dom O , ( F supp (/) ) ) /\ U. dom O C_ dom O /\ ( G supp (/) ) = ( O " U. dom O ) ) -> ( O |` U. dom O ) Isom _E , _E ( U. dom O , ( G supp (/) ) ) )
232	37, 154, 230, 231	syl3anc 1326	. . . . . . . 8 |- ( ph -> ( O |` U. dom O ) Isom _E , _E ( U. dom O , ( G supp (/) ) ) )
233		cantnfp1.k	. . . . . . . . . . 11 |- K = OrdIso ( _E , ( G supp (/) ) )
234	1, 2, 3, 233, 5	cantnfcl 8564	. . . . . . . . . 10 |- ( ph -> ( _E We ( G supp (/) ) /\ dom K e. om ) )
235	234	simpld 475	. . . . . . . . 9 |- ( ph -> _E We ( G supp (/) ) )
236		epse 5097	. . . . . . . . 9 |- _E Se ( G supp (/) )
237	233	oieu 8444	. . . . . . . . 9 |- ( ( _E We ( G supp (/) ) /\ _E Se ( G supp (/) ) ) -> ( ( Ord U. dom O /\ ( O |` U. dom O ) Isom _E , _E ( U. dom O , ( G supp (/) ) ) ) <-> ( U. dom O = dom K /\ ( O |` U. dom O ) = K ) ) )
238	235, 236, 237	sylancl 694	. . . . . . . 8 |- ( ph -> ( ( Ord U. dom O /\ ( O |` U. dom O ) Isom _E , _E ( U. dom O , ( G supp (/) ) ) ) <-> ( U. dom O = dom K /\ ( O |` U. dom O ) = K ) ) )
239	152, 232, 238	mpbi2and 956	. . . . . . 7 |- ( ph -> ( U. dom O = dom K /\ ( O |` U. dom O ) = K ) )
240	239	simpld 475	. . . . . 6 |- ( ph -> U. dom O = dom K )
241	240	fveq2d 6195	. . . . 5 |- ( ph -> ( M ` U. dom O ) = ( M ` dom K ) )
242		eleq1 2689	. . . . . . . . . 10 |- ( x = (/) -> ( x e. dom O <-> (/) e. dom O ) )
243		fveq2 6191	. . . . . . . . . . 11 |- ( x = (/) -> ( H ` x ) = ( H ` (/) ) )
244		fveq2 6191	. . . . . . . . . . . 12 |- ( x = (/) -> ( M ` x ) = ( M ` (/) ) )
245		cantnfp1.m	. . . . . . . . . . . . . 14 |- M = seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( K ` k ) ) .o ( G ` ( K ` k ) ) ) +o z ) ) , (/) )
246	245	seqom0g 7551	. . . . . . . . . . . . 13 |- ( (/) e. _V -> ( M ` (/) ) = (/) )
247	54, 246	ax-mp 5	. . . . . . . . . . . 12 |- ( M ` (/) ) = (/)
248	244, 247	syl6eq 2672	. . . . . . . . . . 11 |- ( x = (/) -> ( M ` x ) = (/) )
249	243, 248	eqeq12d 2637	. . . . . . . . . 10 |- ( x = (/) -> ( ( H ` x ) = ( M ` x ) <-> ( H ` (/) ) = (/) ) )
250	242, 249	imbi12d 334	. . . . . . . . 9 |- ( x = (/) -> ( ( x e. dom O -> ( H ` x ) = ( M ` x ) ) <-> ( (/) e. dom O -> ( H ` (/) ) = (/) ) ) )
251	250	imbi2d 330	. . . . . . . 8 |- ( x = (/) -> ( ( ph -> ( x e. dom O -> ( H ` x ) = ( M ` x ) ) ) <-> ( ph -> ( (/) e. dom O -> ( H ` (/) ) = (/) ) ) ) )
252		eleq1 2689	. . . . . . . . . 10 |- ( x = y -> ( x e. dom O <-> y e. dom O ) )
253		fveq2 6191	. . . . . . . . . . 11 |- ( x = y -> ( H ` x ) = ( H ` y ) )
254		fveq2 6191	. . . . . . . . . . 11 |- ( x = y -> ( M ` x ) = ( M ` y ) )
255	253, 254	eqeq12d 2637	. . . . . . . . . 10 |- ( x = y -> ( ( H ` x ) = ( M ` x ) <-> ( H ` y ) = ( M ` y ) ) )
256	252, 255	imbi12d 334	. . . . . . . . 9 |- ( x = y -> ( ( x e. dom O -> ( H ` x ) = ( M ` x ) ) <-> ( y e. dom O -> ( H ` y ) = ( M ` y ) ) ) )
257	256	imbi2d 330	. . . . . . . 8 |- ( x = y -> ( ( ph -> ( x e. dom O -> ( H ` x ) = ( M ` x ) ) ) <-> ( ph -> ( y e. dom O -> ( H ` y ) = ( M ` y ) ) ) ) )
258		eleq1 2689	. . . . . . . . . 10 |- ( x = suc y -> ( x e. dom O <-> suc y e. dom O ) )
259		fveq2 6191	. . . . . . . . . . 11 |- ( x = suc y -> ( H ` x ) = ( H ` suc y ) )
260		fveq2 6191	. . . . . . . . . . 11 |- ( x = suc y -> ( M ` x ) = ( M ` suc y ) )
261	259, 260	eqeq12d 2637	. . . . . . . . . 10 |- ( x = suc y -> ( ( H ` x ) = ( M ` x ) <-> ( H ` suc y ) = ( M ` suc y ) ) )
262	258, 261	imbi12d 334	. . . . . . . . 9 |- ( x = suc y -> ( ( x e. dom O -> ( H ` x ) = ( M ` x ) ) <-> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) )
263	262	imbi2d 330	. . . . . . . 8 |- ( x = suc y -> ( ( ph -> ( x e. dom O -> ( H ` x ) = ( M ` x ) ) ) <-> ( ph -> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) ) )
264		eleq1 2689	. . . . . . . . . 10 |- ( x = U. dom O -> ( x e. dom O <-> U. dom O e. dom O ) )
265		fveq2 6191	. . . . . . . . . . 11 |- ( x = U. dom O -> ( H ` x ) = ( H ` U. dom O ) )
266		fveq2 6191	. . . . . . . . . . 11 |- ( x = U. dom O -> ( M ` x ) = ( M ` U. dom O ) )
267	265, 266	eqeq12d 2637	. . . . . . . . . 10 |- ( x = U. dom O -> ( ( H ` x ) = ( M ` x ) <-> ( H ` U. dom O ) = ( M ` U. dom O ) ) )
268	264, 267	imbi12d 334	. . . . . . . . 9 |- ( x = U. dom O -> ( ( x e. dom O -> ( H ` x ) = ( M ` x ) ) <-> ( U. dom O e. dom O -> ( H ` U. dom O ) = ( M ` U. dom O ) ) ) )
269	268	imbi2d 330	. . . . . . . 8 |- ( x = U. dom O -> ( ( ph -> ( x e. dom O -> ( H ` x ) = ( M ` x ) ) ) <-> ( ph -> ( U. dom O e. dom O -> ( H ` U. dom O ) = ( M ` U. dom O ) ) ) ) )
270	11	seqom0g 7551	. . . . . . . . . 10 |- ( (/) e. _V -> ( H ` (/) ) = (/) )
271	54, 270	mp1i 13	. . . . . . . . 9 |- ( (/) e. dom O -> ( H ` (/) ) = (/) )
272	271	a1i 11	. . . . . . . 8 |- ( ph -> ( (/) e. dom O -> ( H ` (/) ) = (/) ) )
273		nnord 7073	. . . . . . . . . . . . . . . 16 |- ( dom O e. om -> Ord dom O )
274	17, 273	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> Ord dom O )
275		ordtr 5737	. . . . . . . . . . . . . . 15 |- ( Ord dom O -> Tr dom O )
276	274, 275	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> Tr dom O )
277		trsuc 5810	. . . . . . . . . . . . . 14 |- ( ( Tr dom O /\ suc y e. dom O ) -> y e. dom O )
278	276, 277	sylan 488	. . . . . . . . . . . . 13 |- ( ( ph /\ suc y e. dom O ) -> y e. dom O )
279	278	ex 450	. . . . . . . . . . . 12 |- ( ph -> ( suc y e. dom O -> y e. dom O ) )
280	279	imim1d 82	. . . . . . . . . . 11 |- ( ph -> ( ( y e. dom O -> ( H ` y ) = ( M ` y ) ) -> ( suc y e. dom O -> ( H ` y ) = ( M ` y ) ) ) )
281		oveq2 6658	. . . . . . . . . . . . . 14 |- ( ( H ` y ) = ( M ` y ) -> ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( H ` y ) ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( M ` y ) ) )
282		elnn 7075	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. dom O /\ dom O e. om ) -> y e. om )
283	282	ancoms 469	. . . . . . . . . . . . . . . . . 18 |- ( ( dom O e. om /\ y e. dom O ) -> y e. om )
284	17, 283	sylan 488	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. dom O ) -> y e. om )
285	278, 284	syldan 487	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ suc y e. dom O ) -> y e. om )
286	1, 2, 3, 4, 10, 11	cantnfsuc 8567	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. om ) -> ( H ` suc y ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( H ` y ) ) )
287	285, 286	syldan 487	. . . . . . . . . . . . . . 15 |- ( ( ph /\ suc y e. dom O ) -> ( H ` suc y ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( H ` y ) ) )
288	1, 2, 3, 233, 5, 245	cantnfsuc 8567	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. om ) -> ( M ` suc y ) = ( ( ( A ^o ( K ` y ) ) .o ( G ` ( K ` y ) ) ) +o ( M ` y ) ) )
289	285, 288	syldan 487	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ suc y e. dom O ) -> ( M ` suc y ) = ( ( ( A ^o ( K ` y ) ) .o ( G ` ( K ` y ) ) ) +o ( M ` y ) ) )
290	239	simprd 479	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( O |` U. dom O ) = K )
291	290	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( O |` U. dom O ) ` y ) = ( K ` y ) )
292	291	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ suc y e. dom O ) -> ( ( O |` U. dom O ) ` y ) = ( K ` y ) )
293	14	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( suc y e. dom O <-> suc y e. suc U. dom O ) )
294	293	biimpa 501	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ suc y e. dom O ) -> suc y e. suc U. dom O )
295	152	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ suc y e. dom O ) -> Ord U. dom O )
296		ordsucelsuc 7022	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Ord U. dom O -> ( y e. U. dom O <-> suc y e. suc U. dom O ) )
297	295, 296	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ suc y e. dom O ) -> ( y e. U. dom O <-> suc y e. suc U. dom O ) )
298	294, 297	mpbird 247	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ suc y e. dom O ) -> y e. U. dom O )
299		fvres 6207	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. U. dom O -> ( ( O |` U. dom O ) ` y ) = ( O ` y ) )
300	298, 299	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ suc y e. dom O ) -> ( ( O |` U. dom O ) ` y ) = ( O ` y ) )
301	292, 300	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ suc y e. dom O ) -> ( K ` y ) = ( O ` y ) )
302	301	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ suc y e. dom O ) -> ( A ^o ( K ` y ) ) = ( A ^o ( O ` y ) ) )
303		suppssdm 7308	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( G supp (/) ) C_ dom G
304		fdm 6051	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( G : B --> A -> dom G = B )
305	27, 304	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> dom G = B )
306	303, 305	syl5sseq 3653	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( G supp (/) ) C_ B )
307	306	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ suc y e. dom O ) -> ( G supp (/) ) C_ B )
308	240	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ suc y e. dom O ) -> U. dom O = dom K )
309	298, 308	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ suc y e. dom O ) -> y e. dom K )
310	233	oif 8435	. . . . . . . . . . . . . . . . . . . . . . 23 |- K : dom K --> ( G supp (/) )
311	310	ffvelrni 6358	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. dom K -> ( K ` y ) e. ( G supp (/) ) )
312	309, 311	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ suc y e. dom O ) -> ( K ` y ) e. ( G supp (/) ) )
313	307, 312	sseldd 3604	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ suc y e. dom O ) -> ( K ` y ) e. B )
314	7	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ suc y e. dom O ) -> Y e. A )
315		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21 |- ( G ` ( K ` y ) ) e. _V
316		ifexg 4157	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Y e. A /\ ( G ` ( K ` y ) ) e. _V ) -> if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) e. _V )
317	314, 315, 316	sylancl 694	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ suc y e. dom O ) -> if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) e. _V )
318		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t = ( K ` y ) -> ( t = X <-> ( K ` y ) = X ) )
319		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t = ( K ` y ) -> ( G ` t ) = ( G ` ( K ` y ) ) )
320	318, 319	ifbieq2d 4111	. . . . . . . . . . . . . . . . . . . . 21 |- ( t = ( K ` y ) -> if ( t = X , Y , ( G ` t ) ) = if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) )
321	320, 9	fvmptg 6280	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( K ` y ) e. B /\ if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) e. _V ) -> ( F ` ( K ` y ) ) = if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) )
322	313, 317, 321	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ suc y e. dom O ) -> ( F ` ( K ` y ) ) = if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) )
323	301	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ suc y e. dom O ) -> ( F ` ( K ` y ) ) = ( F ` ( O ` y ) ) )
324	184	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ suc y e. dom O ) -> -. X e. ( G supp (/) ) )
325		nelneq 2725	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( K ` y ) e. ( G supp (/) ) /\ -. X e. ( G supp (/) ) ) -> -. ( K ` y ) = X )
326	312, 324, 325	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ suc y e. dom O ) -> -. ( K ` y ) = X )
327	326	iffalsed 4097	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ suc y e. dom O ) -> if ( ( K ` y ) = X , Y , ( G ` ( K ` y ) ) ) = ( G ` ( K ` y ) ) )
328	322, 323, 327	3eqtr3rd 2665	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ suc y e. dom O ) -> ( G ` ( K ` y ) ) = ( F ` ( O ` y ) ) )
329	302, 328	oveq12d 6668	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ suc y e. dom O ) -> ( ( A ^o ( K ` y ) ) .o ( G ` ( K ` y ) ) ) = ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) )
330	329	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ suc y e. dom O ) -> ( ( ( A ^o ( K ` y ) ) .o ( G ` ( K ` y ) ) ) +o ( M ` y ) ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( M ` y ) ) )
331	289, 330	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( ph /\ suc y e. dom O ) -> ( M ` suc y ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( M ` y ) ) )
332	287, 331	eqeq12d 2637	. . . . . . . . . . . . . 14 |- ( ( ph /\ suc y e. dom O ) -> ( ( H ` suc y ) = ( M ` suc y ) <-> ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( H ` y ) ) = ( ( ( A ^o ( O ` y ) ) .o ( F ` ( O ` y ) ) ) +o ( M ` y ) ) ) )
333	281, 332	syl5ibr 236	. . . . . . . . . . . . 13 |- ( ( ph /\ suc y e. dom O ) -> ( ( H ` y ) = ( M ` y ) -> ( H ` suc y ) = ( M ` suc y ) ) )
334	333	ex 450	. . . . . . . . . . . 12 |- ( ph -> ( suc y e. dom O -> ( ( H ` y ) = ( M ` y ) -> ( H ` suc y ) = ( M ` suc y ) ) ) )
335	334	a2d 29	. . . . . . . . . . 11 |- ( ph -> ( ( suc y e. dom O -> ( H ` y ) = ( M ` y ) ) -> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) )
336	280, 335	syld 47	. . . . . . . . . 10 |- ( ph -> ( ( y e. dom O -> ( H ` y ) = ( M ` y ) ) -> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) )
337	336	a2i 14	. . . . . . . . 9 |- ( ( ph -> ( y e. dom O -> ( H ` y ) = ( M ` y ) ) ) -> ( ph -> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) )
338	337	a1i 11	. . . . . . . 8 |- ( y e. om -> ( ( ph -> ( y e. dom O -> ( H ` y ) = ( M ` y ) ) ) -> ( ph -> ( suc y e. dom O -> ( H ` suc y ) = ( M ` suc y ) ) ) ) )
339	251, 257, 263, 269, 272, 338	finds 7092	. . . . . . 7 |- ( U. dom O e. om -> ( ph -> ( U. dom O e. dom O -> ( H ` U. dom O ) = ( M ` U. dom O ) ) ) )
340	20, 339	mpcom 38	. . . . . 6 |- ( ph -> ( U. dom O e. dom O -> ( H ` U. dom O ) = ( M ` U. dom O ) ) )
341	72, 340	mpd 15	. . . . 5 |- ( ph -> ( H ` U. dom O ) = ( M ` U. dom O ) )
342	1, 2, 3, 233, 5, 245	cantnfval 8565	. . . . 5 |- ( ph -> ( ( A CNF B ) ` G ) = ( M ` dom K ) )
343	241, 341, 342	3eqtr4d 2666	. . . 4 |- ( ph -> ( H ` U. dom O ) = ( ( A CNF B ) ` G ) )
344	150, 343	oveq12d 6668	. . 3 |- ( ph -> ( ( ( A ^o ( O ` U. dom O ) ) .o ( F ` ( O ` U. dom O ) ) ) +o ( H ` U. dom O ) ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )
345	22, 344	eqtrd 2656	. 2 |- ( ph -> ( H ` suc U. dom O ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )
346	12, 15, 345	3eqtrd 2660	1 |- ( ph -> ( ( A CNF B ) ` F ) = ( ( ( A ^o X ) .o Y ) +o ( ( A CNF B ) ` G ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   U.cuni 4436   class class class wbr 4653   |-> cmpt 4729   Tr wtr 4752   _E cep 5028   Se wse 5071   We wwe 5072   `'ccnv 5113   dom cdm 5114   |` cres 5116   "cima 5117   Ord word 5722   Oncon0 5723   suc csuc 5725   Fun wfun 5882   Fn wfn 5883   -->wf 5884   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888   Isom wiso 5889  (class class class)co 6650   |-> cmpt2 6652   omcom 7065   supp csupp 7295  seq_𝜔cseqom 7542   1oc1o 7553   +o coa 7557   .o comu 7558   ^o coe 7559   finSupp cfsupp 8275  OrdIsocoi 8414   CNF ccnf 8558

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-seqom 7543  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-oi 8415  df-cnf 8559

This theorem is referenced by:  cantnfp1  8578