Theorem cantnff 8184

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 5880	. . . 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 4541	. . 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 2453	. . . 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 8173	. . 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 8174	. . . . 5 |- ( ph -> dom ( A CNF B ) = { g e. ( A ^m B ) | g finSupp (/) } )
10	8, 9	syl5eq 2499	. . . 4 |- ( ph -> S = { g e. ( A ^m B ) | g finSupp (/) } )
11	10	mpteq1d 4487	. . 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 2490	. 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 467	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> A e. On )
14	6	adantr 467	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> B e. On )
15		eqid 2453	. . . . . . . 8 |- OrdIso ( _E , ( x supp (/) ) ) = OrdIso ( _E , ( x supp (/) ) )
16		simpr 463	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> x e. S )
17		eqid 2453	. . . . . . . 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 8178	. . . . . . 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 467	. . . . . 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 6323	. . . . . . . . . . 11 |- ( x supp (/) ) e. _V
21	8, 13, 14, 15, 16	cantnfcl 8177	. . . . . . . . . . . 12 |- ( ( ph /\ x e. S ) -> ( _E We ( x supp (/) ) /\ dom OrdIso ( _E , ( x supp (/) ) ) e. om ) )
22	21	simpld 461	. . . . . . . . . . 11 |- ( ( ph /\ x e. S ) -> _E We ( x supp (/) ) )
23	15	oien 8058	. . . . . . . . . . 11 |- ( ( ( x supp (/) ) e. _V /\ _E We ( x supp (/) ) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
24	20, 22, 23	sylancr 670	. . . . . . . . . 10 |- ( ( ph /\ x e. S ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
25	24	adantr 467	. . . . . . . . 9 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
26		suppssdm 6932	. . . . . . . . . . . 12 |- ( x supp (/) ) C_ dom x
27	8, 5, 6	cantnfs 8176	. . . . . . . . . . . . . 14 |- ( ph -> ( x e. S <-> ( x : B --> A /\ x finSupp (/) ) ) )
28	27	simprbda 629	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. S ) -> x : B --> A )
29		fdm 5738	. . . . . . . . . . . . 13 |- ( x : B --> A -> dom x = B )
30	28, 29	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ x e. S ) -> dom x = B )
31	26, 30	syl5sseq 3482	. . . . . . . . . . 11 |- ( ( ph /\ x e. S ) -> ( x supp (/) ) C_ B )
32	31	adantr 467	. . . . . . . . . 10 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x supp (/) ) C_ B )
33		feq3 5717	. . . . . . . . . . . . . 14 |- ( A = (/) -> ( x : B --> A <-> x : B --> (/) ) )
34	28, 33	syl5ibcom 224	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. S ) -> ( A = (/) -> x : B --> (/) ) )
35	34	imp 431	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> x : B --> (/) )
36		f00 5770	. . . . . . . . . . . 12 |- ( x : B --> (/) <-> ( x = (/) /\ B = (/) ) )
37	35, 36	sylib 200	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x = (/) /\ B = (/) ) )
38	37	simprd 465	. . . . . . . . . 10 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> B = (/) )
39		sseq0 3768	. . . . . . . . . 10 |- ( ( ( x supp (/) ) C_ B /\ B = (/) ) -> ( x supp (/) ) = (/) )
40	32, 38, 39	syl2anc 667	. . . . . . . . 9 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x supp (/) ) = (/) )
41	25, 40	breqtrd 4430	. . . . . . . 8 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ (/) )
42		en0 7637	. . . . . . . 8 |- ( dom OrdIso ( _E , ( x supp (/) ) ) ~~ (/) <-> dom OrdIso ( _E , ( x supp (/) ) ) = (/) )
43	41, 42	sylib 200	. . . . . . 7 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) = (/) )
44	43	fveq2d 5874	. . . . . 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 4538	. . . . . . 7 |- (/) e. _V
46	17	seqom0g 7178	. . . . . . 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 13	. . . . . 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 2491	. . . . 5 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) = (/) )
49		el1o 7206	. . . . 5 |- ( ( ( A CNF B ) ` x ) e. 1o <-> ( ( A CNF B ) ` x ) = (/) )
50	48, 49	sylibr 216	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) e. 1o )
51	38	oveq2d 6311	. . . . 5 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o B ) = ( A ^o (/) ) )
52	13	adantr 467	. . . . . 6 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> A e. On )
53		oe0 7229	. . . . . 6 |- ( A e. On -> ( A ^o (/) ) = 1o )
54	52, 53	syl 17	. . . . 5 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o (/) ) = 1o )
55	51, 54	eqtrd 2487	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o B ) = 1o )
56	50, 55	eleqtrrd 2534	. . 3 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
57	13	adantr 467	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> A e. On )
58	14	adantr 467	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> B e. On )
59	16	adantr 467	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> x e. S )
60		on0eln0 5481	. . . . . 6 |- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
61	13, 60	syl 17	. . . . 5 |- ( ( ph /\ x e. S ) -> ( (/) e. A <-> A =/= (/) ) )
62	61	biimpar 488	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> (/) e. A )
63	31	adantr 467	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> ( x supp (/) ) C_ B )
64	8, 57, 58, 59, 62, 58, 63	cantnflt2 8183	. . 3 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
65	56, 64	pm2.61dane 2713	. 2 |- ( ( ph /\ x e. S ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
66	3, 12, 65	fmpt2d 6058	1 |- ( ph -> ( A CNF B ) : S --> ( A ^o B ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1446   e. wcel 1889   =/= wne 2624   {crab 2743   _Vcvv 3047   [_csb 3365   C_ wss 3406   (/)c0 3733   class class class wbr 4405   |-> cmpt 4464   _E cep 4746   We wwe 4795   dom cdm 4837   Oncon0 5426   -->wf 5581   ` cfv 5585  (class class class)co 6295   |-> cmpt2 6297   omcom 6697   supp csupp 6919  seq_𝜔cseqom 7169   1oc1o 7180   +o coa 7184   .o comu 7185   ^o coe 7186   ^m cmap 7477   ~~ cen 7571   finSupp cfsupp 7888  OrdIsocoi 8029   CNF ccnf 8171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-fal 1452  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-se 4797  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-isom 5594  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6698  df-1st 6798  df-2nd 6799  df-supp 6920  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-seqom 7170  df-1o 7187  df-2o 7188  df-oadd 7191  df-omul 7192  df-oexp 7193  df-er 7368  df-map 7479  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-fsupp 7889  df-oi 8030  df-cnf 8172

This theorem is referenced by:  cantnfp1  8191  cantnflem1  8199  cantnflem3  8201  cantnflem4  8202  cantnf  8203