Metamath Proof Explorer

Theorem cantnff

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)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
Assertion cantnff 
|- ( ph -> ( A CNF B ) : S --> ( A ^o B ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 fvex 
 |-  ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) e. _V
5 4 csbex 
 |-  [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) e. _V
6 5 a1i 
 |-  ( ( ph /\ f e. S ) -> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) e. _V )
7 eqid 
 |-  { g e. ( A ^m B ) | g finSupp (/) } = { g e. ( A ^m B ) | g finSupp (/) }
8 7 2 3 cantnffval 
 |-  ( ph -> ( A CNF B ) = ( f e. { g e. ( A ^m B ) | g finSupp (/) } |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )
9 7 2 3 cantnfdm 
 |-  ( ph -> dom ( A CNF B ) = { g e. ( A ^m B ) | g finSupp (/) } )
10 1 9 eqtrid 
 |-  ( ph -> S = { g e. ( A ^m B ) | g finSupp (/) } )
11 10 mpteq1d 
 |-  ( ph -> ( f e. S |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( 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 ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )
12 8 11 eqtr4d 
 |-  ( ph -> ( A CNF B ) = ( f e. S |-> [_ OrdIso ( _E , ( f supp (/) ) ) / h ]_ ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( h ` k ) ) .o ( f ` ( h ` k ) ) ) +o z ) ) , (/) ) ` dom h ) ) )
13 2 adantr 
 |-  ( ( ph /\ x e. S ) -> A e. On )
14 3 adantr 
 |-  ( ( ph /\ x e. S ) -> B e. On )
15 eqid 
 |-  OrdIso ( _E , ( x supp (/) ) ) = OrdIso ( _E , ( x supp (/) ) )
16 simpr 
 |-  ( ( ph /\ x e. S ) -> x e. S )
17 eqid 
 |-  seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` ( OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` ( OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) )
18 1 13 14 15 16 17 cantnfval 
 |-  ( ( ph /\ x e. S ) -> ( ( A CNF B ) ` x ) = ( seqom ( ( 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 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) = ( seqom ( ( 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 
 |-  ( x supp (/) ) e. _V
21 1 13 14 15 16 cantnfcl 
 |-  ( ( ph /\ x e. S ) -> ( _E We ( x supp (/) ) /\ dom OrdIso ( _E , ( x supp (/) ) ) e. _om ) )
22 21 simpld 
 |-  ( ( ph /\ x e. S ) -> _E We ( x supp (/) ) )
23 15 oien 
 |-  ( ( ( x supp (/) ) e. _V /\ _E We ( x supp (/) ) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
24 20 22 23 sylancr 
 |-  ( ( ph /\ x e. S ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
25 24 adantr 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ ( x supp (/) ) )
26 suppssdm 
 |-  ( x supp (/) ) C_ dom x
27 1 2 3 cantnfs 
 |-  ( ph -> ( x e. S <-> ( x : B --> A /\ x finSupp (/) ) ) )
28 27 simprbda 
 |-  ( ( ph /\ x e. S ) -> x : B --> A )
29 26 28 fssdm 
 |-  ( ( ph /\ x e. S ) -> ( x supp (/) ) C_ B )
30 feq3 
 |-  ( A = (/) -> ( x : B --> A <-> x : B --> (/) ) )
31 28 30 syl5ibcom 
 |-  ( ( ph /\ x e. S ) -> ( A = (/) -> x : B --> (/) ) )
32 31 imp 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> x : B --> (/) )
33 f00 
 |-  ( x : B --> (/) <-> ( x = (/) /\ B = (/) ) )
34 32 33 sylib 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x = (/) /\ B = (/) ) )
35 34 simprd 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> B = (/) )
36 sseq0 
 |-  ( ( ( x supp (/) ) C_ B /\ B = (/) ) -> ( x supp (/) ) = (/) )
37 29 35 36 syl2an2r 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( x supp (/) ) = (/) )
38 25 37 breqtrd 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) ~~ (/) )
39 en0 
 |-  ( dom OrdIso ( _E , ( x supp (/) ) ) ~~ (/) <-> dom OrdIso ( _E , ( x supp (/) ) ) = (/) )
40 38 39 sylib 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> dom OrdIso ( _E , ( x supp (/) ) ) = (/) )
41 40 fveq2d 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( seqom ( ( 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 (/) ) ) ) = ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` ( OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) )
42 0ex 
 |-  (/) e. _V
43 17 seqom0g 
 |-  ( (/) e. _V -> ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` ( OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/) )
44 42 43 mp1i 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( x supp (/) ) ) ` k ) ) .o ( x ` ( OrdIso ( _E , ( x supp (/) ) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/) )
45 19 41 44 3eqtrd 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) = (/) )
46 el1o 
 |-  ( ( ( A CNF B ) ` x ) e. 1o <-> ( ( A CNF B ) ` x ) = (/) )
47 45 46 sylibr 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) e. 1o )
48 35 oveq2d 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o B ) = ( A ^o (/) ) )
49 13 adantr 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> A e. On )
50 oe0 
 |-  ( A e. On -> ( A ^o (/) ) = 1o )
51 49 50 syl 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o (/) ) = 1o )
52 48 51 eqtrd 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( A ^o B ) = 1o )
53 47 52 eleqtrrd 
 |-  ( ( ( ph /\ x e. S ) /\ A = (/) ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
54 13 adantr 
 |-  ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> A e. On )
55 14 adantr 
 |-  ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> B e. On )
56 16 adantr 
 |-  ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> x e. S )
57 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
58 13 57 syl 
 |-  ( ( ph /\ x e. S ) -> ( (/) e. A <-> A =/= (/) ) )
59 58 biimpar 
 |-  ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> (/) e. A )
60 29 adantr 
 |-  ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> ( x supp (/) ) C_ B )
61 1 54 55 56 59 55 60 cantnflt2 
 |-  ( ( ( ph /\ x e. S ) /\ A =/= (/) ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
62 53 61 pm2.61dane 
 |-  ( ( ph /\ x e. S ) -> ( ( A CNF B ) ` x ) e. ( A ^o B ) )
63 6 12 62 fmpt2d 
 |-  ( ph -> ( A CNF B ) : S --> ( A ^o B ) )