Theorem cantnff 8091

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 5862	. . . 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 4566	. . 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 2441	. . . 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 8078	. . 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 8079	. . . . 5 |- ( ph -> dom ( A CNF B ) = { g e. ( A ^m B ) | g finSupp (/) } )
10	8, 9	syl5eq 2494	. . . 4 |- ( ph -> S = { g e. ( A ^m B ) | g finSupp (/) } )
11	10	mpteq1d 4514	. . 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 2485	. 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 465	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> A e. On )
14	6	adantr 465	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> B e. On )
15		eqid 2441	. . . . . . . 8 |- OrdIso ( _E , ( x supp (/) ) ) = OrdIso ( _E , ( x supp (/) ) )
16		simpr 461	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> x e. S )
17		eqid 2441	. . . . . . . 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 8085	. . . . . . 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 465	. . . . . 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 6305	. . . . . . . . . . 11 |- ( x supp (/) ) e. _V
21	8, 13, 14, 15, 16	cantnfcl 8084	. . . . . . . . . . . 12 |- ( ( ph /\ x e. S ) -> ( _E We ( x supp (/) ) /\ dom OrdIso ( _E , ( x supp (/) ) ) e. om ) )
22	21	simpld 459	. . . . . . . . . . 11 |- ( ( ph /\ x e. S ) -> _E We ( x supp (/) ) )
23	15	oien 7961	. . . . . . . . . . 11 |- ( ( ( x supp (/) ) e. _V /\ _E We ( x supp (/) ) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
24	20, 22, 23	sylancr 663	. . . . . . . . . 10 |- ( ( ph /\ x e. S ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
25	24	adantr 465	. . . . . . . . 9 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
26		suppssdm 6912	. . . . . . . . . . . 12 |- ( x supp (/) ) C_ dom x
27	8, 5, 6	cantnfs 8083	. . . . . . . . . . . . . 14 |- ( ph -> ( x e. S <-> ( x : B --> A /\ x finSupp (/) ) ) )
28	27	simprbda 623	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. S ) -> x : B --> A )
29		fdm 5721	. . . . . . . . . . . . 13 |- ( x : B --> A -> dom x = B )
30	28, 29	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ x e. S ) -> dom x = B )
31	26, 30	syl5sseq 3534	. . . . . . . . . . 11 |- ( ( ph /\ x e. S ) -> ( x supp (/) ) C_ B )
32	31	adantr 465	. . . . . . . . . 10 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x supp (/) ) C_ B )
33		feq3 5701	. . . . . . . . . . . . . 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 5753	. . . . . . . . . . . 12 |- ( x : B --> (/) <-> ( x = (/) /\ B = (/) ) )
37	35, 36	sylib 196	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x = (/) /\ B = (/) ) )
38	37	simprd 463	. . . . . . . . . 10 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> B = (/) )
39		sseq0 3799	. . . . . . . . . 10 |- ( ( ( x supp (/) ) C_ B /\ B = (/) ) -> ( x supp (/) ) = (/) )
40	32, 38, 39	syl2anc 661	. . . . . . . . 9 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x supp (/) ) = (/) )
41	25, 40	breqtrd 4457	. . . . . . . 8 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ (/) )
42		en0 7576	. . . . . . . 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 5856	. . . . . 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 4563	. . . . . . 7 |- (/) e. _V
46	17	seqom0g 7119	. . . . . . 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 2486	. . . . 5 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) = (/) )
49		el1o 7147	. . . . 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 6293	. . . . 5 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o B ) = ( A ^o (/) ) )
52	13	adantr 465	. . . . . 6 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> A e. On )
53		oe0 7170	. . . . . 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 2482	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o B ) = 1o )
56	50, 55	eleqtrrd 2532	. . 3 |- ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
57	13	adantr 465	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> A e. On )
58	14	adantr 465	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> B e. On )
59	16	adantr 465	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> x e. S )
60		on0eln0 4919	. . . . . 6 |- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
61	13, 60	syl 16	. . . . 5 |- ( ( ph /\ x e. S ) -> ( (/) e. A <-> A =/= (/) ) )
62	61	biimpar 485	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> (/) e. A )
63	31	adantr 465	. . . 4 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> ( x supp (/) ) C_ B )
64	8, 57, 58, 59, 62, 58, 63	cantnflt2 8090	. . 3 |- ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
65	56, 64	pm2.61dane 2759	. 2 |- ( ( ph /\ x e. S ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
66	3, 12, 65	fmpt2d 6042	1 |- ( ph -> ( A CNF B ) : S --> ( A ^o B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1381   e. wcel 1802   =/= wne 2636   {crab 2795   _Vcvv 3093   [_csb 3417   C_ wss 3458   (/)c0 3767   class class class wbr 4433   |-> cmpt 4491   _E cep 4775   We wwe 4823   Oncon0 4864   dom cdm 4985   -->wf 5570   ` cfv 5574  (class class class)co 6277   |-> cmpt2 6279   omcom 6681   supp csupp 6899  seq_𝜔cseqom 7110   1oc1o 7121   +o coa 7125   .o comu 7126   ^o coe 7127   ^m cmap 7418   ~~ cen 7511   finSupp cfsupp 7827  OrdIsocoi 7932   CNF ccnf 8076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-se 4825  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-isom 5583  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-1st 6781  df-2nd 6782  df-supp 6900  df-recs 7040  df-rdg 7074  df-seqom 7111  df-1o 7128  df-2o 7129  df-oadd 7132  df-omul 7133  df-oexp 7134  df-er 7309  df-map 7420  df-en 7515  df-dom 7516  df-sdom 7517  df-fin 7518  df-fsupp 7828  df-oi 7933  df-cnf 8077

This theorem is referenced by:  cantnfp1  8098  cantnflem1  8106  cantnflem3  8108  cantnflem4  8109  cantnf  8110  cantnfp1OLD  8124  cantnflem1OLD  8129  cantnflem3OLD  8130  cantnflem4OLD  8131  cantnfOLD  8132