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 ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
Assertion cantnff ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴 ↑o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 fvex ⊢ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ∈ V
5 4 csbex ⊢ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ∈ V
6 5 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑆 ) → ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ∈ V )
7 eqid ⊢ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ }
8 7 2 3 cantnffval ⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) = ( 𝑓 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) )
9 7 2 3 cantnfdm ⊢ ( 𝜑 → dom ( 𝐴 CNF 𝐵 ) = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
10 1 9 eqtrid ⊢ ( 𝜑 → 𝑆 = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
11 10 mpteq1d ⊢ ( 𝜑 → ( 𝑓 ∈ 𝑆 ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) = ( 𝑓 ∈ { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) )
12 8 11 eqtr4d ⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) = ( 𝑓 ∈ 𝑆 ↦ ⦋ OrdIso ( E , ( 𝑓 supp ∅ ) ) / ℎ ⦌ ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( ℎ ‘ 𝑘 ) ) ·o ( 𝑓 ‘ ( ℎ ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom ℎ ) ) )
13 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ On )
14 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ On )
15 eqid ⊢ OrdIso ( E , ( 𝑥 supp ∅ ) ) = OrdIso ( E , ( 𝑥 supp ∅ ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
17 eqid ⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑥 ‘ ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑥 ‘ ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
18 1 13 14 15 16 17 cantnfval ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑥 ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑥 ‘ ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( 𝑥 supp ∅ ) ) ) )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑥 ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑥 ‘ ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( 𝑥 supp ∅ ) ) ) )
20 ovex ⊢ ( 𝑥 supp ∅ ) ∈ V
21 1 13 14 15 16 cantnfcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( E We ( 𝑥 supp ∅ ) ∧ dom OrdIso ( E , ( 𝑥 supp ∅ ) ) ∈ ω ) )
22 21 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → E We ( 𝑥 supp ∅ ) )
23 15 oien ⊢ ( ( ( 𝑥 supp ∅ ) ∈ V ∧ E We ( 𝑥 supp ∅ ) ) → dom OrdIso ( E , ( 𝑥 supp ∅ ) ) ≈ ( 𝑥 supp ∅ ) )
24 20 22 23 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → dom OrdIso ( E , ( 𝑥 supp ∅ ) ) ≈ ( 𝑥 supp ∅ ) )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → dom OrdIso ( E , ( 𝑥 supp ∅ ) ) ≈ ( 𝑥 supp ∅ ) )
26 suppssdm ⊢ ( 𝑥 supp ∅ ) ⊆ dom 𝑥
27 1 2 3 cantnfs ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↔ ( 𝑥 : 𝐵 ⟶ 𝐴 ∧ 𝑥 finSupp ∅ ) ) )
28 27 simprbda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 : 𝐵 ⟶ 𝐴 )
29 26 28 fssdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 supp ∅ ) ⊆ 𝐵 )
30 feq3 ⊢ ( 𝐴 = ∅ → ( 𝑥 : 𝐵 ⟶ 𝐴 ↔ 𝑥 : 𝐵 ⟶ ∅ ) )
31 28 30 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐴 = ∅ → 𝑥 : 𝐵 ⟶ ∅ ) )
32 31 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → 𝑥 : 𝐵 ⟶ ∅ )
33 f00 ⊢ ( 𝑥 : 𝐵 ⟶ ∅ ↔ ( 𝑥 = ∅ ∧ 𝐵 = ∅ ) )
34 32 33 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( 𝑥 = ∅ ∧ 𝐵 = ∅ ) )
35 34 simprd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → 𝐵 = ∅ )
36 sseq0 ⊢ ( ( ( 𝑥 supp ∅ ) ⊆ 𝐵 ∧ 𝐵 = ∅ ) → ( 𝑥 supp ∅ ) = ∅ )
37 29 35 36 syl2an2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( 𝑥 supp ∅ ) = ∅ )
38 25 37 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → dom OrdIso ( E , ( 𝑥 supp ∅ ) ) ≈ ∅ )
39 en0 ⊢ ( dom OrdIso ( E , ( 𝑥 supp ∅ ) ) ≈ ∅ ↔ dom OrdIso ( E , ( 𝑥 supp ∅ ) ) = ∅ )
40 38 39 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → dom OrdIso ( E , ( 𝑥 supp ∅ ) ) = ∅ )
41 40 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑥 ‘ ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( 𝑥 supp ∅ ) ) ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑥 ‘ ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) )
42 0ex ⊢ ∅ ∈ V
43 17 seqom0g ⊢ ( ∅ ∈ V → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑥 ‘ ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) = ∅ )
44 42 43 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝑥 ‘ ( OrdIso ( E , ( 𝑥 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ ∅ ) = ∅ )
45 19 41 44 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑥 ) = ∅ )
46 el1o ⊢ ( ( ( 𝐴 CNF 𝐵 ) ‘ 𝑥 ) ∈ 1o ↔ ( ( 𝐴 CNF 𝐵 ) ‘ 𝑥 ) = ∅ )
47 45 46 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑥 ) ∈ 1o )
48 35 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = ( 𝐴 ↑o ∅ ) )
49 13 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → 𝐴 ∈ On )
50 oe0 ⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o ∅ ) = 1o )
51 49 50 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o ∅ ) = 1o )
52 48 51 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = 1o )
53 47 52 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 = ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑥 ) ∈ ( 𝐴 ↑o 𝐵 ) )
54 13 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ On )
55 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 ≠ ∅ ) → 𝐵 ∈ On )
56 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 ≠ ∅ ) → 𝑥 ∈ 𝑆 )
57 on0eln0 ⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
58 13 57 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
59 58 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 ≠ ∅ ) → ∅ ∈ 𝐴 )
60 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 ≠ ∅ ) → ( 𝑥 supp ∅ ) ⊆ 𝐵 )
61 1 54 55 56 59 55 60 cantnflt2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝐴 ≠ ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑥 ) ∈ ( 𝐴 ↑o 𝐵 ) )
62 53 61 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝑥 ) ∈ ( 𝐴 ↑o 𝐵 ) )
63 6 12 62 fmpt2d ⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴 ↑o 𝐵 ) )