Theorem cantnff 7870

Description: The CNF function is a function from finitely supported functions from B to A, to the ordinal exponential A ^o B. (Contributed by Mario Carneiro, 28-May-2015.)

Hypotheses

Ref	Expression
cantnfs.s	|- S = dom ( A CNF B )
cantnfs.a	|- ( ph -> A e. On )
cantnfs.b	|- ( ph -> B e. On )

Assertion

Ref	Expression
cantnff	|- ( ph -> ( A CNF B ) : S --> ( A ^o B ) )

Proof of Theorem cantnff

Dummy variables f g h k x z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fvex 5689	. . . 4 |- (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) e. _V
2	1	csbex 4413	. . 3 |- [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) e. _V
3	2	a1i 11	. 2 |- ( ( ph /\ f e. S ) -> [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) e. _V )
4		eqid 2433	. . . 4 |- { g e. ( A ^m B ) | g finSupp (/) } = { g e. ( A ^m B ) | g finSupp (/) }
5		cantnfs.a	. . . 4 |- ( ph -> A e. On )
6		cantnfs.b	. . . 4 |- ( ph -> B e. On )
7	4, 5, 6	cantnffval 7857	. . 3 |- ( ph -> ( A CNF B ) = ( f e. { g e. ( A ^m B ) | g finSupp (/) } |-> [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )
8		cantnfs.s	. . . . 5 |- S = dom ( A CNF B )
9	4, 5, 6	cantnfdm 7858	. . . . 5 |- ( ph -> dom ( A CNF B ) = { g e. ( A ^m B ) | g finSupp (/) } )
10	8, 9	syl5eq 2477	. . . 4 |- ( ph -> S = { g e. ( A ^m B ) | g finSupp (/) } )
11	10	mpteq1d 4361	. . 3 |- ( ph -> ( f e. S |-> [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) = ( f e. { g e. ( A ^m B ) | g finSupp (/) } |-> [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )
12	7, 11	eqtr4d 2468	. 2 |- ( ph -> ( A CNF B ) = ( f e. S |-> [_OrdIso ( _E , ( f supp (/) ) ) / h ]_ (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )
13	5	adantr 462	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> A e. On )
14	6	adantr 462	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> B e. On )
15		eqid 2433	. . . . . . . 8 |- OrdIso ( _E , ( x supp (/) ) ) = OrdIso ( _E , ( x supp (/) ) )
16		simpr 458	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> x e. S )
17		eqid 2433	. . . . . . . 8 |- seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) )
18	8, 13, 14, 15, 16, 17	cantnfval 7864	. . . . . . 7 |- ( ( ph /\ x e. S ) -> ( ( A CNF B ) ` x ) = (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( x supp (/) ) ) ) )
19	18	adantr 462	. . . . . 6 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) = (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( x supp (/) ) ) ) )
20		ovex 6105	. . . . . . . . . . 11 |- ( x supp (/) ) e. _V
21	8, 13, 14, 15, 16	cantnfcl 7863	. . . . . . . . . . . 12 |- ( ( ph /\ x e. S ) -> ( _E We ( x supp (/) ) /\ dom OrdIso ( _E , ( x supp (/) ) ) e. om ) )
22	21	simpld 456	. . . . . . . . . . 11 |- ( ( ph /\ x e. S ) -> _E We ( x supp (/) ) )
23	15	oien 7740	. . . . . . . . . . 11 |- ( ( ( x supp (/) ) e. _V /\ _E We ( x supp (/) ) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
24	20, 22, 23	sylancr 656	. . . . . . . . . 10 |- ( ( ph /\ x e. S ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
25	24	adantr 462	. . . . . . . . 9 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
26		suppssdm 6692	. . . . . . . . . . . 12 |- ( x supp (/) ) C_ dom x
27	8, 5, 6	cantnfs 7862	. . . . . . . . . . . . . 14 |- ( ph -> ( x e. S <-> ( x : B --> A /\ x finSupp (/) ) ) )
28	27	simprbda 618	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. S ) -> x : B --> A )
29		fdm 5551	. . . . . . . . . . . . 13 |- ( x : B --> A -> dom x = B )
30	28, 29	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ x e. S ) -> dom x = B )
31	26, 30	syl5sseq 3392	. . . . . . . . . . 11 |- ( ( ph /\ x e. S ) -> ( x supp (/) ) C_ B )
32	31	adantr 462	. . . . . . . . . 10 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x supp (/) ) C_ B )
33		feq3 5532	. . . . . . . . . . . . . 14 |- ( A = (/) -> ( x : B --> A <-> x : B --> (/) ) )
34	28, 33	syl5ibcom 220	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. S ) -> ( A = (/) -> x : B --> (/) ) )
35	34	imp 429	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> x : B --> (/) )
36		f00 5581	. . . . . . . . . . . 12 |- ( x : B --> (/) <-> ( x = (/) /\ B = (/) ) )
37	35, 36	sylib 196	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x = (/) /\ B = (/) ) )
38	37	simprd 460	. . . . . . . . . 10 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> B = (/) )
39		sseq0 3657	. . . . . . . . . 10 |- ( ( ( x supp (/) ) C_ B /\ B = (/) ) -> ( x supp (/) ) = (/) )
40	32, 38, 39	syl2anc 654	. . . . . . . . 9 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x supp (/) ) = (/) )
41	25, 40	breqtrd 4304	. . . . . . . 8 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ (/) )
42		en0 7360	. . . . . . . 8 |- ( dom OrdIso ( _E , ( x supp (/) ) ) ~~ (/) <-> dom OrdIso ( _E , ( x supp (/) ) ) = (/) )
43	41, 42	sylib 196	. . . . . . 7 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) = (/) )
44	43	fveq2d 5683	. . . . . 6 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , ( x supp (/) ) ) ) = (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) )
45		0ex 4410	. . . . . . 7 |- (/) e. _V
46	17	seqom0g 6897	. . . . . . 7 |- ( (/) e. _V -> (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/) )
47	45, 46	mp1i 12	. . . . . 6 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` (OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/) )
48	19, 44, 47	3eqtrd 2469	. . . . 5 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) = (/) )
49		el1o 6927	. . . . 5 |- ( ( ( A CNF B ) ` x ) e. 1o <-> ( ( A CNF B ) ` x ) = (/) )
50	48, 49	sylibr 212	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) e. 1o )
51	38	oveq2d 6096	. . . . 5 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o B ) = ( A ^o (/) ) )
52	13	adantr 462	. . . . . 6 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> A e. On )
53		oe0 6950	. . . . . 6 |- ( A e. On -> ( A ^o (/) ) = 1o )
54	52, 53	syl 16	. . . . 5 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o (/) ) = 1o )
55	51, 54	eqtrd 2465	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o B ) = 1o )
56	50, 55	eleqtrrd 2510	. . 3 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
57	13	adantr 462	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> A e. On )
58	14	adantr 462	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> B e. On )
59	16	adantr 462	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> x e. S )
60		on0eln0 4761	. . . . . 6 |- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
61	13, 60	syl 16	. . . . 5 |- ( ( ph /\ x e. S ) -> ( (/) e. A <-> A =/= (/) ) )
62	61	biimpar 482	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> (/) e. A )
63	31	adantr 462	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> ( x supp (/) ) C_ B )
64	8, 57, 58, 59, 62, 58, 63	cantnflt2 7869	. . 3 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
65	56, 64	pm2.61dane 2679	. 2 |- ( ( ph /\ x e. S ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
66	3, 12, 65	fmpt2d 5860	1 |- ( ph -> ( A CNF B ) : S --> ( A ^o B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1362   e. wcel 1755   =/= wne 2596   {crab 2709   _Vcvv 2962   [_csb 3276   C_ wss 3316   (/)c0 3625   class class class wbr 4280   e. cmpt 4338   _E cep 4617   We wwe 4665   Oncon0 4706   dom cdm 4827   -->wf 5402   ` cfv 5406  (class class class)co 6080   e. cmpt2 6082   omcom 6465   supp csupp 6679  seq_𝜔cseqom 6888   1oc1o 6901   +o coa 6905   .o comu 6906   ^o coe 6907   ^m cmap 7202   ~~ cen 7295   finSupp cfsupp 7608  OrdIsocoi 7711   CNF ccnf 7855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-fal 1368  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-1st 6566  df-2nd 6567  df-supp 6680  df-recs 6818  df-rdg 6852  df-seqom 6889  df-1o 6908  df-2o 6909  df-oadd 6912  df-omul 6913  df-oexp 6914  df-er 7089  df-map 7204  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-fsupp 7609  df-oi 7712  df-cnf 7856

This theorem is referenced by:  cantnfp1  7877  cantnflem1  7885  cantnflem3  7887  cantnflem4  7888  cantnf  7889  cantnfp1OLD  7903  cantnflem1OLD  7908  cantnflem3OLD  7909  cantnflem4OLD  7910  cantnfOLD  7911