This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cantnflem3

Description: Lemma for cantnf . Here we show existence of Cantor normal forms. Assuming (by transfinite induction) that every number less than C has a normal form, we can use oeeu to factor C into the form ( ( A ^o X ) .o Y ) +o Z where 0 < Y < A and Z < ( A ^o X ) (and a fortiori X < B ). Then since Z < ( A ^o X ) <_ ( A ^o X ) .o Y <_ C , Z has a normal form, and by appending the term ( A ^o X ) .o Y using cantnfp1 we get a normal form for C . (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
cantnf.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ↑o 𝐵 ) )
cantnf.s ⊢ ( 𝜑 → 𝐶 ⊆ ran ( 𝐴 CNF 𝐵 ) )
cantnf.e ⊢ ( 𝜑 → ∅ ∈ 𝐶 )
cantnf.x ⊢ 𝑋 = ∪ ∩ { 𝑐 ∈ On ∣ 𝐶 ∈ ( 𝐴 ↑o 𝑐 ) }
cantnf.p ⊢ 𝑃 = ( ℩ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴 ↑o 𝑋 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑎 ) +o 𝑏 ) = 𝐶 ) )
cantnf.y ⊢ 𝑌 = ( 1st ‘ 𝑃 )
cantnf.z ⊢ 𝑍 = ( 2nd ‘ 𝑃 )
cantnf.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
cantnf.v ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) = 𝑍 )
cantnf.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) )
Assertion cantnflem3 ( 𝜑 → 𝐶 ∈ ran ( 𝐴 CNF 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
5 cantnf.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ↑o 𝐵 ) )
6 cantnf.s ⊢ ( 𝜑 → 𝐶 ⊆ ran ( 𝐴 CNF 𝐵 ) )
7 cantnf.e ⊢ ( 𝜑 → ∅ ∈ 𝐶 )
8 cantnf.x ⊢ 𝑋 = ∪ ∩ { 𝑐 ∈ On ∣ 𝐶 ∈ ( 𝐴 ↑o 𝑐 ) }
9 cantnf.p ⊢ 𝑃 = ( ℩ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( 𝐴 ↑o 𝑋 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑎 ) +o 𝑏 ) = 𝐶 ) )
10 cantnf.y ⊢ 𝑌 = ( 1st ‘ 𝑃 )
11 cantnf.z ⊢ 𝑍 = ( 2nd ‘ 𝑃 )
12 cantnf.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
13 cantnf.v ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) = 𝑍 )
14 cantnf.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) )
15 1 2 3 4 5 6 7 cantnflem2 ⊢ ( 𝜑 → ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐶 ∈ ( On ∖ 1o ) ) )
16 eqid ⊢ 𝑋 = 𝑋
17 eqid ⊢ 𝑌 = 𝑌
18 eqid ⊢ 𝑍 = 𝑍
19 16 17 18 3pm3.2i ⊢ ( 𝑋 = 𝑋 ∧ 𝑌 = 𝑌 ∧ 𝑍 = 𝑍 )
20 8 9 10 11 oeeui ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐶 ∈ ( On ∖ 1o ) ) → ( ( ( 𝑋 ∈ On ∧ 𝑌 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) ∧ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) = 𝐶 ) ↔ ( 𝑋 = 𝑋 ∧ 𝑌 = 𝑌 ∧ 𝑍 = 𝑍 ) ) )
21 19 20 mpbiri ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐶 ∈ ( On ∖ 1o ) ) → ( ( 𝑋 ∈ On ∧ 𝑌 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) ∧ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) = 𝐶 ) )
22 15 21 syl ⊢ ( 𝜑 → ( ( 𝑋 ∈ On ∧ 𝑌 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) ∧ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) = 𝐶 ) )
23 22 simpld ⊢ ( 𝜑 → ( 𝑋 ∈ On ∧ 𝑌 ∈ ( 𝐴 ∖ 1o ) ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) )
24 23 simp1d ⊢ ( 𝜑 → 𝑋 ∈ On )
25 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ On ) → ( 𝐴 ↑o 𝑋 ) ∈ On )
26 2 24 25 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↑o 𝑋 ) ∈ On )
27 23 simp2d ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 ∖ 1o ) )
28 27 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
29 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ On )
30 2 28 29 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ On )
31 dif1o ⊢ ( 𝑌 ∈ ( 𝐴 ∖ 1o ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ≠ ∅ ) )
32 31 simprbi ⊢ ( 𝑌 ∈ ( 𝐴 ∖ 1o ) → 𝑌 ≠ ∅ )
33 27 32 syl ⊢ ( 𝜑 → 𝑌 ≠ ∅ )
34 on0eln0 ⊢ ( 𝑌 ∈ On → ( ∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅ ) )
35 30 34 syl ⊢ ( 𝜑 → ( ∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅ ) )
36 33 35 mpbird ⊢ ( 𝜑 → ∅ ∈ 𝑌 )
37 omword1 ⊢ ( ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ 𝑌 ∈ On ) ∧ ∅ ∈ 𝑌 ) → ( 𝐴 ↑o 𝑋 ) ⊆ ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) )
38 26 30 36 37 syl21anc ⊢ ( 𝜑 → ( 𝐴 ↑o 𝑋 ) ⊆ ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) )
39 omcl ⊢ ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ 𝑌 ∈ On ) → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ∈ On )
40 26 30 39 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ∈ On )
41 23 simp3d ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) )
42 onelon ⊢ ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) → 𝑍 ∈ On )
43 26 41 42 syl2anc ⊢ ( 𝜑 → 𝑍 ∈ On )
44 oaword1 ⊢ ( ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ∈ On ∧ 𝑍 ∈ On ) → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ⊆ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) )
45 40 43 44 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ⊆ ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) )
46 22 simprd ⊢ ( 𝜑 → ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) = 𝐶 )
47 45 46 sseqtrd ⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) ⊆ 𝐶 )
48 38 47 sstrd ⊢ ( 𝜑 → ( 𝐴 ↑o 𝑋 ) ⊆ 𝐶 )
49 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
50 2 3 49 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↑o 𝐵 ) ∈ On )
51 ontr2 ⊢ ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ ( 𝐴 ↑o 𝐵 ) ∈ On ) → ( ( ( 𝐴 ↑o 𝑋 ) ⊆ 𝐶 ∧ 𝐶 ∈ ( 𝐴 ↑o 𝐵 ) ) → ( 𝐴 ↑o 𝑋 ) ∈ ( 𝐴 ↑o 𝐵 ) ) )
52 26 50 51 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 ↑o 𝑋 ) ⊆ 𝐶 ∧ 𝐶 ∈ ( 𝐴 ↑o 𝐵 ) ) → ( 𝐴 ↑o 𝑋 ) ∈ ( 𝐴 ↑o 𝐵 ) ) )
53 48 5 52 mp2and ⊢ ( 𝜑 → ( 𝐴 ↑o 𝑋 ) ∈ ( 𝐴 ↑o 𝐵 ) )
54 15 simpld ⊢ ( 𝜑 → 𝐴 ∈ ( On ∖ 2o ) )
55 oeord ⊢ ( ( 𝑋 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝑋 ∈ 𝐵 ↔ ( 𝐴 ↑o 𝑋 ) ∈ ( 𝐴 ↑o 𝐵 ) ) )
56 24 3 54 55 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ ( 𝐴 ↑o 𝑋 ) ∈ ( 𝐴 ↑o 𝐵 ) ) )
57 53 56 mpbird ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
58 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝐴 ∈ On )
59 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝐵 ∈ On )
60 suppssdm ⊢ ( 𝐺 supp ∅ ) ⊆ dom 𝐺
61 1 2 3 cantnfs ⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) )
62 12 61 mpbid ⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) )
63 62 simpld ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
64 60 63 fssdm ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ 𝐵 )
65 64 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝑥 ∈ 𝐵 )
66 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
67 59 65 66 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝑥 ∈ On )
68 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 ↑o 𝑥 ) ∈ On )
69 58 67 68 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝐴 ↑o 𝑥 ) ∈ On )
70 63 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝐺 : 𝐵 ⟶ 𝐴 )
71 70 65 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝐴 )
72 onelon ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ On )
73 58 71 72 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝐺 ‘ 𝑥 ) ∈ On )
74 63 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
75 7 elexd ⊢ ( 𝜑 → ∅ ∈ V )
76 elsuppfn ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V ) → ( 𝑥 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑥 ) ≠ ∅ ) ) )
77 74 3 75 76 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑥 ) ≠ ∅ ) ) )
78 77 simplbda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝐺 ‘ 𝑥 ) ≠ ∅ )
79 on0eln0 ⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ On → ( ∅ ∈ ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) ≠ ∅ ) )
80 73 79 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ∅ ∈ ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) ≠ ∅ ) )
81 78 80 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ∅ ∈ ( 𝐺 ‘ 𝑥 ) )
82 omword1 ⊢ ( ( ( ( 𝐴 ↑o 𝑥 ) ∈ On ∧ ( 𝐺 ‘ 𝑥 ) ∈ On ) ∧ ∅ ∈ ( 𝐺 ‘ 𝑥 ) ) → ( 𝐴 ↑o 𝑥 ) ⊆ ( ( 𝐴 ↑o 𝑥 ) ·o ( 𝐺 ‘ 𝑥 ) ) )
83 69 73 81 82 syl21anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝐴 ↑o 𝑥 ) ⊆ ( ( 𝐴 ↑o 𝑥 ) ·o ( 𝐺 ‘ 𝑥 ) ) )
84 eqid ⊢ OrdIso ( E , ( 𝐺 supp ∅ ) ) = OrdIso ( E , ( 𝐺 supp ∅ ) )
85 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝐺 ∈ 𝑆 )
86 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 𝑧 ) ) , ∅ )
87 1 58 59 84 85 86 65 cantnfle ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ( 𝐴 ↑o 𝑥 ) ·o ( 𝐺 ‘ 𝑥 ) ) ⊆ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) )
88 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) = 𝑍 )
89 87 88 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ( 𝐴 ↑o 𝑥 ) ·o ( 𝐺 ‘ 𝑥 ) ) ⊆ 𝑍 )
90 83 89 sstrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝐴 ↑o 𝑥 ) ⊆ 𝑍 )
91 41 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) )
92 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝐴 ↑o 𝑋 ) ∈ On )
93 ontr2 ⊢ ( ( ( 𝐴 ↑o 𝑥 ) ∈ On ∧ ( 𝐴 ↑o 𝑋 ) ∈ On ) → ( ( ( 𝐴 ↑o 𝑥 ) ⊆ 𝑍 ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) → ( 𝐴 ↑o 𝑥 ) ∈ ( 𝐴 ↑o 𝑋 ) ) )
94 69 92 93 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ( ( 𝐴 ↑o 𝑥 ) ⊆ 𝑍 ∧ 𝑍 ∈ ( 𝐴 ↑o 𝑋 ) ) → ( 𝐴 ↑o 𝑥 ) ∈ ( 𝐴 ↑o 𝑋 ) ) )
95 90 91 94 mp2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝐴 ↑o 𝑥 ) ∈ ( 𝐴 ↑o 𝑋 ) )
96 24 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝑋 ∈ On )
97 54 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝐴 ∈ ( On ∖ 2o ) )
98 oeord ⊢ ( ( 𝑥 ∈ On ∧ 𝑋 ∈ On ∧ 𝐴 ∈ ( On ∖ 2o ) ) → ( 𝑥 ∈ 𝑋 ↔ ( 𝐴 ↑o 𝑥 ) ∈ ( 𝐴 ↑o 𝑋 ) ) )
99 67 96 97 98 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝑥 ∈ 𝑋 ↔ ( 𝐴 ↑o 𝑥 ) ∈ ( 𝐴 ↑o 𝑋 ) ) )
100 95 99 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝑥 ∈ 𝑋 )
101 100 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 supp ∅ ) → 𝑥 ∈ 𝑋 ) )
102 101 ssrdv ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ 𝑋 )
103 1 2 3 12 57 28 102 14 cantnfp1 ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) ) )
104 103 simprd ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) )
105 13 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o 𝑍 ) )
106 104 105 46 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = 𝐶 )
107 1 2 3 cantnff ⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴 ↑o 𝐵 ) )
108 107 ffnd ⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) Fn 𝑆 )
109 103 simpld ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
110 fnfvelrn ⊢ ( ( ( 𝐴 CNF 𝐵 ) Fn 𝑆 ∧ 𝐹 ∈ 𝑆 ) → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ran ( 𝐴 CNF 𝐵 ) )
111 108 109 110 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ran ( 𝐴 CNF 𝐵 ) )
112 106 111 eqeltrrd ⊢ ( 𝜑 → 𝐶 ∈ ran ( 𝐴 CNF 𝐵 ) )