MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cantnflem3 Structured version   Visualization version   GIF version

Theorem cantnflem3 8761
Description: Lemma for cantnf 8763. Here we show existence of Cantor normal forms. Assuming (by transfinite induction) that every number less than 𝐶 has a normal form, we can use oeeu 7852 to factor 𝐶 into the form ((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 𝑍 where 0 < 𝑌 < 𝐴 and 𝑍 < (𝐴𝑜 𝑋) (and a fortiori 𝑋 < 𝐵). Then since 𝑍 < (𝐴𝑜 𝑋) ≤ (𝐴𝑜 𝑋) ·𝑜 𝑌𝐶, 𝑍 has a normal form, and by appending the term (𝐴𝑜 𝑋) ·𝑜 𝑌 using cantnfp1 8751 we get a normal form for 𝐶. (Contributed by Mario Carneiro, 28-May-2015.)
Hypotheses
Ref Expression
cantnfs.s 𝑆 = dom (𝐴 CNF 𝐵)
cantnfs.a (𝜑𝐴 ∈ On)
cantnfs.b (𝜑𝐵 ∈ On)
oemapval.t 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))}
cantnf.c (𝜑𝐶 ∈ (𝐴𝑜 𝐵))
cantnf.s (𝜑𝐶 ⊆ ran (𝐴 CNF 𝐵))
cantnf.e (𝜑 → ∅ ∈ 𝐶)
cantnf.x 𝑋 = {𝑐 ∈ On ∣ 𝐶 ∈ (𝐴𝑜 𝑐)}
cantnf.p 𝑃 = (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 𝑋)(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑎) +𝑜 𝑏) = 𝐶))
cantnf.y 𝑌 = (1st𝑃)
cantnf.z 𝑍 = (2nd𝑃)
cantnf.g (𝜑𝐺𝑆)
cantnf.v (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍)
cantnf.f 𝐹 = (𝑡𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)))
Assertion
Ref Expression
cantnflem3 (𝜑𝐶 ∈ ran (𝐴 CNF 𝐵))
Distinct variable groups:   𝑡,𝑐,𝑤,𝑥,𝑦,𝑧,𝐵   𝑎,𝑏,𝑐,𝑑,𝑤,𝑥,𝑦,𝑧,𝐶   𝑡,𝑎,𝐴,𝑏,𝑐,𝑑,𝑤,𝑥,𝑦,𝑧   𝑇,𝑐,𝑡   𝑤,𝐹,𝑥,𝑦,𝑧   𝑆,𝑐,𝑡,𝑥,𝑦,𝑧   𝑡,𝑍,𝑥,𝑦,𝑧   𝐺,𝑐,𝑡,𝑤,𝑥,𝑦,𝑧   𝜑,𝑡,𝑥,𝑦,𝑧   𝑡,𝑌,𝑤,𝑥,𝑦,𝑧   𝑋,𝑎,𝑏,𝑑,𝑡,𝑤,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑤,𝑎,𝑏,𝑐,𝑑)   𝐵(𝑎,𝑏,𝑑)   𝐶(𝑡)   𝑃(𝑥,𝑦,𝑧,𝑤,𝑡,𝑎,𝑏,𝑐,𝑑)   𝑆(𝑤,𝑎,𝑏,𝑑)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑎,𝑏,𝑑)   𝐹(𝑡,𝑎,𝑏,𝑐,𝑑)   𝐺(𝑎,𝑏,𝑑)   𝑋(𝑐)   𝑌(𝑎,𝑏,𝑐,𝑑)   𝑍(𝑤,𝑎,𝑏,𝑐,𝑑)

Proof of Theorem cantnflem3
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 cantnfs.s . . . . 5 𝑆 = dom (𝐴 CNF 𝐵)
2 cantnfs.a . . . . 5 (𝜑𝐴 ∈ On)
3 cantnfs.b . . . . 5 (𝜑𝐵 ∈ On)
4 cantnf.g . . . . 5 (𝜑𝐺𝑆)
5 oemapval.t . . . . . . . . . . . . . 14 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))}
6 cantnf.c . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ (𝐴𝑜 𝐵))
7 cantnf.s . . . . . . . . . . . . . 14 (𝜑𝐶 ⊆ ran (𝐴 CNF 𝐵))
8 cantnf.e . . . . . . . . . . . . . 14 (𝜑 → ∅ ∈ 𝐶)
91, 2, 3, 5, 6, 7, 8cantnflem2 8760 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐶 ∈ (On ∖ 1𝑜)))
10 eqid 2760 . . . . . . . . . . . . . . 15 𝑋 = 𝑋
11 eqid 2760 . . . . . . . . . . . . . . 15 𝑌 = 𝑌
12 eqid 2760 . . . . . . . . . . . . . . 15 𝑍 = 𝑍
1310, 11, 123pm3.2i 1424 . . . . . . . . . . . . . 14 (𝑋 = 𝑋𝑌 = 𝑌𝑍 = 𝑍)
14 cantnf.x . . . . . . . . . . . . . . 15 𝑋 = {𝑐 ∈ On ∣ 𝐶 ∈ (𝐴𝑜 𝑐)}
15 cantnf.p . . . . . . . . . . . . . . 15 𝑃 = (℩𝑑𝑎 ∈ On ∃𝑏 ∈ (𝐴𝑜 𝑋)(𝑑 = ⟨𝑎, 𝑏⟩ ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑎) +𝑜 𝑏) = 𝐶))
16 cantnf.y . . . . . . . . . . . . . . 15 𝑌 = (1st𝑃)
17 cantnf.z . . . . . . . . . . . . . . 15 𝑍 = (2nd𝑃)
1814, 15, 16, 17oeeui 7851 . . . . . . . . . . . . . 14 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐶 ∈ (On ∖ 1𝑜)) → (((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑍 ∈ (𝐴𝑜 𝑋)) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 𝑍) = 𝐶) ↔ (𝑋 = 𝑋𝑌 = 𝑌𝑍 = 𝑍)))
1913, 18mpbiri 248 . . . . . . . . . . . . 13 ((𝐴 ∈ (On ∖ 2𝑜) ∧ 𝐶 ∈ (On ∖ 1𝑜)) → ((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑍 ∈ (𝐴𝑜 𝑋)) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 𝑍) = 𝐶))
209, 19syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑍 ∈ (𝐴𝑜 𝑋)) ∧ (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 𝑍) = 𝐶))
2120simpld 477 . . . . . . . . . . 11 (𝜑 → (𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑍 ∈ (𝐴𝑜 𝑋)))
2221simp1d 1137 . . . . . . . . . 10 (𝜑𝑋 ∈ On)
23 oecl 7786 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴𝑜 𝑋) ∈ On)
242, 22, 23syl2anc 696 . . . . . . . . 9 (𝜑 → (𝐴𝑜 𝑋) ∈ On)
2521simp2d 1138 . . . . . . . . . . 11 (𝜑𝑌 ∈ (𝐴 ∖ 1𝑜))
2625eldifad 3727 . . . . . . . . . 10 (𝜑𝑌𝐴)
27 onelon 5909 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑌𝐴) → 𝑌 ∈ On)
282, 26, 27syl2anc 696 . . . . . . . . 9 (𝜑𝑌 ∈ On)
29 dif1o 7749 . . . . . . . . . . . 12 (𝑌 ∈ (𝐴 ∖ 1𝑜) ↔ (𝑌𝐴𝑌 ≠ ∅))
3029simprbi 483 . . . . . . . . . . 11 (𝑌 ∈ (𝐴 ∖ 1𝑜) → 𝑌 ≠ ∅)
3125, 30syl 17 . . . . . . . . . 10 (𝜑𝑌 ≠ ∅)
32 on0eln0 5941 . . . . . . . . . . 11 (𝑌 ∈ On → (∅ ∈ 𝑌𝑌 ≠ ∅))
3328, 32syl 17 . . . . . . . . . 10 (𝜑 → (∅ ∈ 𝑌𝑌 ≠ ∅))
3431, 33mpbird 247 . . . . . . . . 9 (𝜑 → ∅ ∈ 𝑌)
35 omword1 7822 . . . . . . . . 9 ((((𝐴𝑜 𝑋) ∈ On ∧ 𝑌 ∈ On) ∧ ∅ ∈ 𝑌) → (𝐴𝑜 𝑋) ⊆ ((𝐴𝑜 𝑋) ·𝑜 𝑌))
3624, 28, 34, 35syl21anc 1476 . . . . . . . 8 (𝜑 → (𝐴𝑜 𝑋) ⊆ ((𝐴𝑜 𝑋) ·𝑜 𝑌))
37 omcl 7785 . . . . . . . . . . 11 (((𝐴𝑜 𝑋) ∈ On ∧ 𝑌 ∈ On) → ((𝐴𝑜 𝑋) ·𝑜 𝑌) ∈ On)
3824, 28, 37syl2anc 696 . . . . . . . . . 10 (𝜑 → ((𝐴𝑜 𝑋) ·𝑜 𝑌) ∈ On)
3921simp3d 1139 . . . . . . . . . . 11 (𝜑𝑍 ∈ (𝐴𝑜 𝑋))
40 onelon 5909 . . . . . . . . . . 11 (((𝐴𝑜 𝑋) ∈ On ∧ 𝑍 ∈ (𝐴𝑜 𝑋)) → 𝑍 ∈ On)
4124, 39, 40syl2anc 696 . . . . . . . . . 10 (𝜑𝑍 ∈ On)
42 oaword1 7801 . . . . . . . . . 10 ((((𝐴𝑜 𝑋) ·𝑜 𝑌) ∈ On ∧ 𝑍 ∈ On) → ((𝐴𝑜 𝑋) ·𝑜 𝑌) ⊆ (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 𝑍))
4338, 41, 42syl2anc 696 . . . . . . . . 9 (𝜑 → ((𝐴𝑜 𝑋) ·𝑜 𝑌) ⊆ (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 𝑍))
4420simprd 482 . . . . . . . . 9 (𝜑 → (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 𝑍) = 𝐶)
4543, 44sseqtrd 3782 . . . . . . . 8 (𝜑 → ((𝐴𝑜 𝑋) ·𝑜 𝑌) ⊆ 𝐶)
4636, 45sstrd 3754 . . . . . . 7 (𝜑 → (𝐴𝑜 𝑋) ⊆ 𝐶)
47 oecl 7786 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝑜 𝐵) ∈ On)
482, 3, 47syl2anc 696 . . . . . . . 8 (𝜑 → (𝐴𝑜 𝐵) ∈ On)
49 ontr2 5933 . . . . . . . 8 (((𝐴𝑜 𝑋) ∈ On ∧ (𝐴𝑜 𝐵) ∈ On) → (((𝐴𝑜 𝑋) ⊆ 𝐶𝐶 ∈ (𝐴𝑜 𝐵)) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 𝐵)))
5024, 48, 49syl2anc 696 . . . . . . 7 (𝜑 → (((𝐴𝑜 𝑋) ⊆ 𝐶𝐶 ∈ (𝐴𝑜 𝐵)) → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 𝐵)))
5146, 6, 50mp2and 717 . . . . . 6 (𝜑 → (𝐴𝑜 𝑋) ∈ (𝐴𝑜 𝐵))
529simpld 477 . . . . . . 7 (𝜑𝐴 ∈ (On ∖ 2𝑜))
53 oeord 7837 . . . . . . 7 ((𝑋 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ (On ∖ 2𝑜)) → (𝑋𝐵 ↔ (𝐴𝑜 𝑋) ∈ (𝐴𝑜 𝐵)))
5422, 3, 52, 53syl3anc 1477 . . . . . 6 (𝜑 → (𝑋𝐵 ↔ (𝐴𝑜 𝑋) ∈ (𝐴𝑜 𝐵)))
5551, 54mpbird 247 . . . . 5 (𝜑𝑋𝐵)
562adantr 472 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐴 ∈ On)
573adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐵 ∈ On)
58 suppssdm 7476 . . . . . . . . . . . . . . 15 (𝐺 supp ∅) ⊆ dom 𝐺
591, 2, 3cantnfs 8736 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
604, 59mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
6160simpld 477 . . . . . . . . . . . . . . . 16 (𝜑𝐺:𝐵𝐴)
62 fdm 6212 . . . . . . . . . . . . . . . 16 (𝐺:𝐵𝐴 → dom 𝐺 = 𝐵)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (𝜑 → dom 𝐺 = 𝐵)
6458, 63syl5sseq 3794 . . . . . . . . . . . . . 14 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
6564sselda 3744 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑥𝐵)
66 onelon 5909 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑥𝐵) → 𝑥 ∈ On)
6757, 65, 66syl2anc 696 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑥 ∈ On)
68 oecl 7786 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴𝑜 𝑥) ∈ On)
6956, 67, 68syl2anc 696 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴𝑜 𝑥) ∈ On)
7061adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐺:𝐵𝐴)
7170, 65ffvelrnd 6523 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐺𝑥) ∈ 𝐴)
72 onelon 5909 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ (𝐺𝑥) ∈ 𝐴) → (𝐺𝑥) ∈ On)
7356, 71, 72syl2anc 696 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐺𝑥) ∈ On)
74 ffn 6206 . . . . . . . . . . . . . . 15 (𝐺:𝐵𝐴𝐺 Fn 𝐵)
7561, 74syl 17 . . . . . . . . . . . . . 14 (𝜑𝐺 Fn 𝐵)
76 0ex 4942 . . . . . . . . . . . . . . 15 ∅ ∈ V
7776a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ∅ ∈ V)
78 elsuppfn 7471 . . . . . . . . . . . . . 14 ((𝐺 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑥 ∈ (𝐺 supp ∅) ↔ (𝑥𝐵 ∧ (𝐺𝑥) ≠ ∅)))
7975, 3, 77, 78syl3anc 1477 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (𝐺 supp ∅) ↔ (𝑥𝐵 ∧ (𝐺𝑥) ≠ ∅)))
8079simplbda 655 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐺𝑥) ≠ ∅)
81 on0eln0 5941 . . . . . . . . . . . . 13 ((𝐺𝑥) ∈ On → (∅ ∈ (𝐺𝑥) ↔ (𝐺𝑥) ≠ ∅))
8273, 81syl 17 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (∅ ∈ (𝐺𝑥) ↔ (𝐺𝑥) ≠ ∅))
8380, 82mpbird 247 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ∅ ∈ (𝐺𝑥))
84 omword1 7822 . . . . . . . . . . 11 ((((𝐴𝑜 𝑥) ∈ On ∧ (𝐺𝑥) ∈ On) ∧ ∅ ∈ (𝐺𝑥)) → (𝐴𝑜 𝑥) ⊆ ((𝐴𝑜 𝑥) ·𝑜 (𝐺𝑥)))
8569, 73, 83, 84syl21anc 1476 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴𝑜 𝑥) ⊆ ((𝐴𝑜 𝑥) ·𝑜 (𝐺𝑥)))
86 eqid 2760 . . . . . . . . . . . 12 OrdIso( E , (𝐺 supp ∅)) = OrdIso( E , (𝐺 supp ∅))
874adantr 472 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐺𝑆)
88 eqid 2760 . . . . . . . . . . . 12 seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , (𝐺 supp ∅))‘𝑘)) ·𝑜 (𝐺‘(OrdIso( E , (𝐺 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (OrdIso( E , (𝐺 supp ∅))‘𝑘)) ·𝑜 (𝐺‘(OrdIso( E , (𝐺 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)
891, 56, 57, 86, 87, 88, 65cantnfle 8741 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ((𝐴𝑜 𝑥) ·𝑜 (𝐺𝑥)) ⊆ ((𝐴 CNF 𝐵)‘𝐺))
90 cantnf.v . . . . . . . . . . . 12 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍)
9190adantr 472 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍)
9289, 91sseqtrd 3782 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → ((𝐴𝑜 𝑥) ·𝑜 (𝐺𝑥)) ⊆ 𝑍)
9385, 92sstrd 3754 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴𝑜 𝑥) ⊆ 𝑍)
9439adantr 472 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑍 ∈ (𝐴𝑜 𝑋))
9524adantr 472 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴𝑜 𝑋) ∈ On)
96 ontr2 5933 . . . . . . . . . 10 (((𝐴𝑜 𝑥) ∈ On ∧ (𝐴𝑜 𝑋) ∈ On) → (((𝐴𝑜 𝑥) ⊆ 𝑍𝑍 ∈ (𝐴𝑜 𝑋)) → (𝐴𝑜 𝑥) ∈ (𝐴𝑜 𝑋)))
9769, 95, 96syl2anc 696 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (((𝐴𝑜 𝑥) ⊆ 𝑍𝑍 ∈ (𝐴𝑜 𝑋)) → (𝐴𝑜 𝑥) ∈ (𝐴𝑜 𝑋)))
9893, 94, 97mp2and 717 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝐴𝑜 𝑥) ∈ (𝐴𝑜 𝑋))
9922adantr 472 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑋 ∈ On)
10052adantr 472 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝐴 ∈ (On ∖ 2𝑜))
101 oeord 7837 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖ 2𝑜)) → (𝑥𝑋 ↔ (𝐴𝑜 𝑥) ∈ (𝐴𝑜 𝑋)))
10267, 99, 100, 101syl3anc 1477 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → (𝑥𝑋 ↔ (𝐴𝑜 𝑥) ∈ (𝐴𝑜 𝑋)))
10398, 102mpbird 247 . . . . . . 7 ((𝜑𝑥 ∈ (𝐺 supp ∅)) → 𝑥𝑋)
104103ex 449 . . . . . 6 (𝜑 → (𝑥 ∈ (𝐺 supp ∅) → 𝑥𝑋))
105104ssrdv 3750 . . . . 5 (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)
106 cantnf.f . . . . 5 𝐹 = (𝑡𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)))
1071, 2, 3, 4, 55, 26, 105, 106cantnfp1 8751 . . . 4 (𝜑 → (𝐹𝑆 ∧ ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺))))
108107simprd 482 . . 3 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))
10990oveq2d 6829 . . 3 (𝜑 → (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 𝑍))
110108, 109, 443eqtrd 2798 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = 𝐶)
1111, 2, 3cantnff 8744 . . . 4 (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
112 ffn 6206 . . . 4 ((𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵) → (𝐴 CNF 𝐵) Fn 𝑆)
113111, 112syl 17 . . 3 (𝜑 → (𝐴 CNF 𝐵) Fn 𝑆)
114107simpld 477 . . 3 (𝜑𝐹𝑆)
115 fnfvelrn 6519 . . 3 (((𝐴 CNF 𝐵) Fn 𝑆𝐹𝑆) → ((𝐴 CNF 𝐵)‘𝐹) ∈ ran (𝐴 CNF 𝐵))
116113, 114, 115syl2anc 696 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ran (𝐴 CNF 𝐵))
117110, 116eqeltrrd 2840 1 (𝜑𝐶 ∈ ran (𝐴 CNF 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  {crab 3054  Vcvv 3340  cdif 3712  wss 3715  c0 4058  ifcif 4230  cop 4327   cuni 4588   cint 4627   class class class wbr 4804  {copab 4864  cmpt 4881   E cep 5178  dom cdm 5266  ran crn 5267  Oncon0 5884  cio 6010   Fn wfn 6044  wf 6045  cfv 6049  (class class class)co 6813  cmpt2 6815  1st c1st 7331  2nd c2nd 7332   supp csupp 7463  seq𝜔cseqom 7711  1𝑜c1o 7722  2𝑜c2o 7723   +𝑜 coa 7726   ·𝑜 comu 7727  𝑜 coe 7728   finSupp cfsupp 8440  OrdIsocoi 8579   CNF ccnf 8731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-seqom 7712  df-1o 7729  df-2o 7730  df-oadd 7733  df-omul 7734  df-oexp 7735  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-oi 8580  df-cnf 8732
This theorem is referenced by:  cantnflem4  8762
  Copyright terms: Public domain W3C validator