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

Theorem cantnfle 8825
Description: A lower bound on the CNF function. Since ((𝐴 CNF 𝐵)‘𝐹) is defined as the sum of (𝐴𝑜 𝑥) ·𝑜 (𝐹𝑥) over all 𝑥 in the support of 𝐹, it is larger than any of these terms (and all other terms are zero, so we can extend the statement to all 𝐶𝐵 instead of just those 𝐶 in the support). (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 28-Jun-2019.)
Hypotheses
Ref Expression
cantnfs.s 𝑆 = dom (𝐴 CNF 𝐵)
cantnfs.a (𝜑𝐴 ∈ On)
cantnfs.b (𝜑𝐵 ∈ On)
cantnfcl.g 𝐺 = OrdIso( E , (𝐹 supp ∅))
cantnfcl.f (𝜑𝐹𝑆)
cantnfval.h 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝐺𝑘)) ·𝑜 (𝐹‘(𝐺𝑘))) +𝑜 𝑧)), ∅)
cantnfle.c (𝜑𝐶𝐵)
Assertion
Ref Expression
cantnfle (𝜑 → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹))
Distinct variable groups:   𝑧,𝑘,𝐵   𝑧,𝐶   𝐴,𝑘,𝑧   𝑘,𝐹,𝑧   𝑆,𝑘,𝑧   𝑘,𝐺,𝑧   𝜑,𝑘,𝑧
Allowed substitution hints:   𝐶(𝑘)   𝐻(𝑧,𝑘)

Proof of Theorem cantnfle
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6892 . . 3 ((𝐹𝐶) = ∅ → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) = ((𝐴𝑜 𝐶) ·𝑜 ∅))
21sseq1d 3840 . 2 ((𝐹𝐶) = ∅ → (((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹) ↔ ((𝐴𝑜 𝐶) ·𝑜 ∅) ⊆ ((𝐴 CNF 𝐵)‘𝐹)))
3 cantnfs.b . . . . . . . . . 10 (𝜑𝐵 ∈ On)
4 suppssdm 7552 . . . . . . . . . . 11 (𝐹 supp ∅) ⊆ dom 𝐹
5 cantnfcl.f . . . . . . . . . . . . 13 (𝜑𝐹𝑆)
6 cantnfs.s . . . . . . . . . . . . . 14 𝑆 = dom (𝐴 CNF 𝐵)
7 cantnfs.a . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ On)
86, 7, 3cantnfs 8820 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
95, 8mpbid 223 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
109simpld 484 . . . . . . . . . . 11 (𝜑𝐹:𝐵𝐴)
114, 10fssdm 6282 . . . . . . . . . 10 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
123, 11ssexd 5013 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ∈ V)
13 cantnfcl.g . . . . . . . . . . 11 𝐺 = OrdIso( E , (𝐹 supp ∅))
146, 7, 3, 13, 5cantnfcl 8821 . . . . . . . . . 10 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
1514simpld 484 . . . . . . . . 9 (𝜑 → E We (𝐹 supp ∅))
1613oiiso 8691 . . . . . . . . 9 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
1712, 15, 16syl2anc 575 . . . . . . . 8 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
18 isof1o 6807 . . . . . . . 8 (𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) → 𝐺:dom 𝐺1-1-onto→(𝐹 supp ∅))
1917, 18syl 17 . . . . . . 7 (𝜑𝐺:dom 𝐺1-1-onto→(𝐹 supp ∅))
2019adantr 468 . . . . . 6 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐺:dom 𝐺1-1-onto→(𝐹 supp ∅))
21 f1ocnv 6375 . . . . . 6 (𝐺:dom 𝐺1-1-onto→(𝐹 supp ∅) → 𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺)
22 f1of 6363 . . . . . 6 (𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺𝐺:(𝐹 supp ∅)⟶dom 𝐺)
2320, 21, 223syl 18 . . . . 5 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐺:(𝐹 supp ∅)⟶dom 𝐺)
24 cantnfle.c . . . . . . 7 (𝜑𝐶𝐵)
2524anim1i 604 . . . . . 6 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → (𝐶𝐵 ∧ (𝐹𝐶) ≠ ∅))
2610adantr 468 . . . . . . . 8 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐹:𝐵𝐴)
2726ffnd 6267 . . . . . . 7 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐹 Fn 𝐵)
283adantr 468 . . . . . . 7 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐵 ∈ On)
29 0ex 4997 . . . . . . . 8 ∅ ∈ V
3029a1i 11 . . . . . . 7 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ∅ ∈ V)
31 elsuppfn 7547 . . . . . . 7 ((𝐹 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝐶 ∈ (𝐹 supp ∅) ↔ (𝐶𝐵 ∧ (𝐹𝐶) ≠ ∅)))
3227, 28, 30, 31syl3anc 1483 . . . . . 6 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → (𝐶 ∈ (𝐹 supp ∅) ↔ (𝐶𝐵 ∧ (𝐹𝐶) ≠ ∅)))
3325, 32mpbird 248 . . . . 5 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐶 ∈ (𝐹 supp ∅))
3423, 33ffvelrnd 6592 . . . 4 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → (𝐺𝐶) ∈ dom 𝐺)
3514simprd 485 . . . . . 6 (𝜑 → dom 𝐺 ∈ ω)
3635adantr 468 . . . . 5 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → dom 𝐺 ∈ ω)
37 eqimss 3865 . . . . . . . . . 10 (𝑥 = dom 𝐺𝑥 ⊆ dom 𝐺)
3837biantrurd 524 . . . . . . . . 9 (𝑥 = dom 𝐺 → ((𝐺𝐶) ∈ 𝑥 ↔ (𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥)))
39 eleq2 2885 . . . . . . . . 9 (𝑥 = dom 𝐺 → ((𝐺𝐶) ∈ 𝑥 ↔ (𝐺𝐶) ∈ dom 𝐺))
4038, 39bitr3d 272 . . . . . . . 8 (𝑥 = dom 𝐺 → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) ↔ (𝐺𝐶) ∈ dom 𝐺))
41 fveq2 6418 . . . . . . . . 9 (𝑥 = dom 𝐺 → (𝐻𝑥) = (𝐻‘dom 𝐺))
4241sseq2d 3841 . . . . . . . 8 (𝑥 = dom 𝐺 → (((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑥) ↔ ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺)))
4340, 42imbi12d 335 . . . . . . 7 (𝑥 = dom 𝐺 → (((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑥)) ↔ ((𝐺𝐶) ∈ dom 𝐺 → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺))))
4443imbi2d 331 . . . . . 6 (𝑥 = dom 𝐺 → (((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑥))) ↔ ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐺𝐶) ∈ dom 𝐺 → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺)))))
45 sseq1 3834 . . . . . . . . 9 (𝑥 = ∅ → (𝑥 ⊆ dom 𝐺 ↔ ∅ ⊆ dom 𝐺))
46 eleq2 2885 . . . . . . . . 9 (𝑥 = ∅ → ((𝐺𝐶) ∈ 𝑥 ↔ (𝐺𝐶) ∈ ∅))
4745, 46anbi12d 618 . . . . . . . 8 (𝑥 = ∅ → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) ↔ (∅ ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ ∅)))
48 fveq2 6418 . . . . . . . . 9 (𝑥 = ∅ → (𝐻𝑥) = (𝐻‘∅))
4948sseq2d 3841 . . . . . . . 8 (𝑥 = ∅ → (((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑥) ↔ ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘∅)))
5047, 49imbi12d 335 . . . . . . 7 (𝑥 = ∅ → (((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑥)) ↔ ((∅ ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ ∅) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘∅))))
51 sseq1 3834 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥 ⊆ dom 𝐺𝑦 ⊆ dom 𝐺))
52 eleq2 2885 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝐺𝐶) ∈ 𝑥 ↔ (𝐺𝐶) ∈ 𝑦))
5351, 52anbi12d 618 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) ↔ (𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)))
54 fveq2 6418 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
5554sseq2d 3841 . . . . . . . 8 (𝑥 = 𝑦 → (((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑥) ↔ ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)))
5653, 55imbi12d 335 . . . . . . 7 (𝑥 = 𝑦 → (((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑥)) ↔ ((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦))))
57 sseq1 3834 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝑥 ⊆ dom 𝐺 ↔ suc 𝑦 ⊆ dom 𝐺))
58 eleq2 2885 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝐺𝐶) ∈ 𝑥 ↔ (𝐺𝐶) ∈ suc 𝑦))
5957, 58anbi12d 618 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) ↔ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ suc 𝑦)))
60 fveq2 6418 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐻𝑥) = (𝐻‘suc 𝑦))
6160sseq2d 3841 . . . . . . . 8 (𝑥 = suc 𝑦 → (((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑥) ↔ ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
6259, 61imbi12d 335 . . . . . . 7 (𝑥 = suc 𝑦 → (((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑥)) ↔ ((suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ suc 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
63 noel 4131 . . . . . . . . . 10 ¬ (𝐺𝐶) ∈ ∅
6463pm2.21i 117 . . . . . . . . 9 ((𝐺𝐶) ∈ ∅ → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘∅))
6564adantl 469 . . . . . . . 8 ((∅ ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ ∅) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘∅))
6665a1i 11 . . . . . . 7 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((∅ ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ ∅) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘∅)))
67 fvex 6431 . . . . . . . . . . . 12 (𝐺𝐶) ∈ V
6867elsuc 6020 . . . . . . . . . . 11 ((𝐺𝐶) ∈ suc 𝑦 ↔ ((𝐺𝐶) ∈ 𝑦 ∨ (𝐺𝐶) = 𝑦))
69 sssucid 6028 . . . . . . . . . . . . . . . . 17 𝑦 ⊆ suc 𝑦
70 sstr 3817 . . . . . . . . . . . . . . . . 17 ((𝑦 ⊆ suc 𝑦 ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ⊆ dom 𝐺)
7169, 70mpan 673 . . . . . . . . . . . . . . . 16 (suc 𝑦 ⊆ dom 𝐺𝑦 ⊆ dom 𝐺)
7271ad2antrl 710 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)) → 𝑦 ⊆ dom 𝐺)
73 simprr 780 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)) → (𝐺𝐶) ∈ 𝑦)
74 pm2.27 42 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)))
7572, 73, 74syl2anc 575 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)))
76 cantnfval.h . . . . . . . . . . . . . . . . . . . . 21 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝐺𝑘)) ·𝑜 (𝐹‘(𝐺𝑘))) +𝑜 𝑧)), ∅)
7776cantnfvalf 8819 . . . . . . . . . . . . . . . . . . . 20 𝐻:ω⟶On
7877ffvelrni 6590 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ω → (𝐻𝑦) ∈ On)
7978ad2antlr 709 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻𝑦) ∈ On)
807ad3antrrr 712 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐴 ∈ On)
813ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐵 ∈ On)
8211ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹 supp ∅) ⊆ 𝐵)
83 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → suc 𝑦 ⊆ dom 𝐺)
84 sucidg 6029 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ω → 𝑦 ∈ suc 𝑦)
8584ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ∈ suc 𝑦)
8683, 85sseldd 3810 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ∈ dom 𝐺)
8713oif 8684 . . . . . . . . . . . . . . . . . . . . . . . 24 𝐺:dom 𝐺⟶(𝐹 supp ∅)
8887ffvelrni 6590 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ dom 𝐺 → (𝐺𝑦) ∈ (𝐹 supp ∅))
8986, 88syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺𝑦) ∈ (𝐹 supp ∅))
9082, 89sseldd 3810 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺𝑦) ∈ 𝐵)
91 onelon 5975 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 ∈ On ∧ (𝐺𝑦) ∈ 𝐵) → (𝐺𝑦) ∈ On)
9281, 90, 91syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺𝑦) ∈ On)
93 oecl 7864 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ (𝐺𝑦) ∈ On) → (𝐴𝑜 (𝐺𝑦)) ∈ On)
9480, 92, 93syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐴𝑜 (𝐺𝑦)) ∈ On)
9510ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐹:𝐵𝐴)
9695, 90ffvelrnd 6592 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹‘(𝐺𝑦)) ∈ 𝐴)
97 onelon 5975 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ (𝐹‘(𝐺𝑦)) ∈ 𝐴) → (𝐹‘(𝐺𝑦)) ∈ On)
9880, 96, 97syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹‘(𝐺𝑦)) ∈ On)
99 omcl 7863 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑜 (𝐺𝑦)) ∈ On ∧ (𝐹‘(𝐺𝑦)) ∈ On) → ((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) ∈ On)
10094, 98, 99syl2anc 575 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) ∈ On)
101 oaword2 7880 . . . . . . . . . . . . . . . . . 18 (((𝐻𝑦) ∈ On ∧ ((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) ∈ On) → (𝐻𝑦) ⊆ (((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) +𝑜 (𝐻𝑦)))
10279, 100, 101syl2anc 575 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻𝑦) ⊆ (((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) +𝑜 (𝐻𝑦)))
103 simplll 782 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝜑)
104 simplr 776 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ∈ ω)
1056, 7, 3, 13, 5, 76cantnfsuc 8824 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) +𝑜 (𝐻𝑦)))
106103, 104, 105syl2anc 575 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻‘suc 𝑦) = (((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) +𝑜 (𝐻𝑦)))
107102, 106sseqtr4d 3850 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻𝑦) ⊆ (𝐻‘suc 𝑦))
108 sstr 3817 . . . . . . . . . . . . . . . . 17 ((((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦) ∧ (𝐻𝑦) ⊆ (𝐻‘suc 𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))
109108expcom 400 . . . . . . . . . . . . . . . 16 ((𝐻𝑦) ⊆ (𝐻‘suc 𝑦) → (((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
110107, 109syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
111110adantrr 699 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)) → (((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
11275, 111syld 47 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
113112expr 446 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐺𝐶) ∈ 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
114 simprr 780 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐺𝐶) = 𝑦)
115114fveq2d 6422 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐺‘(𝐺𝐶)) = (𝐺𝑦))
116 f1ocnvfv2 6767 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺:dom 𝐺1-1-onto→(𝐹 supp ∅) ∧ 𝐶 ∈ (𝐹 supp ∅)) → (𝐺‘(𝐺𝐶)) = 𝐶)
11720, 33, 116syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → (𝐺‘(𝐺𝐶)) = 𝐶)
118117ad2antrr 708 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐺‘(𝐺𝐶)) = 𝐶)
119115, 118eqtr3d 2853 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐺𝑦) = 𝐶)
120119oveq2d 6900 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐴𝑜 (𝐺𝑦)) = (𝐴𝑜 𝐶))
121119fveq2d 6422 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐹‘(𝐺𝑦)) = (𝐹𝐶))
122120, 121oveq12d 6902 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → ((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) = ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)))
123 oaword1 7879 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) ∈ On ∧ (𝐻𝑦) ∈ On) → ((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) ⊆ (((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) +𝑜 (𝐻𝑦)))
124100, 79, 123syl2anc 575 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) ⊆ (((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) +𝑜 (𝐻𝑦)))
125124adantrr 699 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → ((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) ⊆ (((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) +𝑜 (𝐻𝑦)))
126122, 125eqsstr3d 3848 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) +𝑜 (𝐻𝑦)))
127106adantrr 699 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐻‘suc 𝑦) = (((𝐴𝑜 (𝐺𝑦)) ·𝑜 (𝐹‘(𝐺𝑦))) +𝑜 (𝐻𝑦)))
128126, 127sseqtr4d 3850 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))
129128expr 446 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐺𝐶) = 𝑦 → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
130129a1dd 50 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐺𝐶) = 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
131113, 130jaod 877 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (((𝐺𝐶) ∈ 𝑦 ∨ (𝐺𝐶) = 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
13268, 131syl5bi 233 . . . . . . . . . 10 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐺𝐶) ∈ suc 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
133132expimpd 443 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ suc 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
134133com23 86 . . . . . . . 8 (((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ suc 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
135134expcom 400 . . . . . . 7 (𝑦 ∈ ω → ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ suc 𝑦) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))))
13650, 56, 62, 66, 135finds2 7334 . . . . . 6 (𝑥 ∈ ω → ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻𝑥))))
13744, 136vtoclga 3476 . . . . 5 (dom 𝐺 ∈ ω → ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐺𝐶) ∈ dom 𝐺 → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺))))
13836, 137mpcom 38 . . . 4 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐺𝐶) ∈ dom 𝐺 → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺)))
13934, 138mpd 15 . . 3 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺))
1406, 7, 3, 13, 5, 76cantnfval 8822 . . . 4 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺))
141140adantr 468 . . 3 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺))
142139, 141sseqtr4d 3850 . 2 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹))
143 onelon 5975 . . . . . 6 ((𝐵 ∈ On ∧ 𝐶𝐵) → 𝐶 ∈ On)
1443, 24, 143syl2anc 575 . . . . 5 (𝜑𝐶 ∈ On)
145 oecl 7864 . . . . 5 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴𝑜 𝐶) ∈ On)
1467, 144, 145syl2anc 575 . . . 4 (𝜑 → (𝐴𝑜 𝐶) ∈ On)
147 om0 7844 . . . 4 ((𝐴𝑜 𝐶) ∈ On → ((𝐴𝑜 𝐶) ·𝑜 ∅) = ∅)
148146, 147syl 17 . . 3 (𝜑 → ((𝐴𝑜 𝐶) ·𝑜 ∅) = ∅)
149 0ss 4181 . . 3 ∅ ⊆ ((𝐴 CNF 𝐵)‘𝐹)
150148, 149syl6eqss 3863 . 2 (𝜑 → ((𝐴𝑜 𝐶) ·𝑜 ∅) ⊆ ((𝐴 CNF 𝐵)‘𝐹))
1512, 142, 150pm2.61ne 3074 1 (𝜑 → ((𝐴𝑜 𝐶) ·𝑜 (𝐹𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2157  wne 2989  Vcvv 3402  wss 3780  c0 4127   class class class wbr 4855   E cep 5236   We wwe 5282  ccnv 5323  dom cdm 5324  Oncon0 5950  suc csuc 5952   Fn wfn 6106  wf 6107  1-1-ontowf1o 6110  cfv 6111   Isom wiso 6112  (class class class)co 6884  cmpt2 6886  ωcom 7305   supp csupp 7539  seq𝜔cseqom 7788   +𝑜 coa 7803   ·𝑜 comu 7804  𝑜 coe 7805   finSupp cfsupp 8524  OrdIsocoi 8663   CNF ccnf 8815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-om 7306  df-1st 7408  df-2nd 7409  df-supp 7540  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-seqom 7789  df-1o 7806  df-oadd 7810  df-omul 7811  df-oexp 7812  df-er 7989  df-map 8104  df-en 8203  df-dom 8204  df-sdom 8205  df-fin 8206  df-fsupp 8525  df-oi 8664  df-cnf 8816
This theorem is referenced by:  cantnflem3  8845
  Copyright terms: Public domain W3C validator