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

Theorem cantnfle 9708
Description: A lower bound on the CNF function. Since ((𝐴 CNF 𝐵)‘𝐹) is defined as the sum of (𝐴o 𝑥) ·o (𝐹𝑥) 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 ↦ (((𝐴o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
cantnfle.c (𝜑𝐶𝐵)
Assertion
Ref Expression
cantnfle (𝜑 → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ ((𝐴 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 7438 . . 3 ((𝐹𝐶) = ∅ → ((𝐴o 𝐶) ·o (𝐹𝐶)) = ((𝐴o 𝐶) ·o ∅))
21sseq1d 4026 . 2 ((𝐹𝐶) = ∅ → (((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹) ↔ ((𝐴o 𝐶) ·o ∅) ⊆ ((𝐴 CNF 𝐵)‘𝐹)))
3 ovexd 7465 . . . . . . . . 9 (𝜑 → (𝐹 supp ∅) ∈ V)
4 cantnfs.s . . . . . . . . . . 11 𝑆 = dom (𝐴 CNF 𝐵)
5 cantnfs.a . . . . . . . . . . 11 (𝜑𝐴 ∈ On)
6 cantnfs.b . . . . . . . . . . 11 (𝜑𝐵 ∈ On)
7 cantnfcl.g . . . . . . . . . . 11 𝐺 = OrdIso( E , (𝐹 supp ∅))
8 cantnfcl.f . . . . . . . . . . 11 (𝜑𝐹𝑆)
94, 5, 6, 7, 8cantnfcl 9704 . . . . . . . . . 10 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
109simpld 494 . . . . . . . . 9 (𝜑 → E We (𝐹 supp ∅))
117oiiso 9574 . . . . . . . . 9 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
123, 10, 11syl2anc 584 . . . . . . . 8 (𝜑𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)))
13 isof1o 7342 . . . . . . . 8 (𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) → 𝐺:dom 𝐺1-1-onto→(𝐹 supp ∅))
1412, 13syl 17 . . . . . . 7 (𝜑𝐺:dom 𝐺1-1-onto→(𝐹 supp ∅))
1514adantr 480 . . . . . 6 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐺:dom 𝐺1-1-onto→(𝐹 supp ∅))
16 f1ocnv 6860 . . . . . 6 (𝐺:dom 𝐺1-1-onto→(𝐹 supp ∅) → 𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺)
17 f1of 6848 . . . . . 6 (𝐺:(𝐹 supp ∅)–1-1-onto→dom 𝐺𝐺:(𝐹 supp ∅)⟶dom 𝐺)
1815, 16, 173syl 18 . . . . 5 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐺:(𝐹 supp ∅)⟶dom 𝐺)
19 cantnfle.c . . . . . . 7 (𝜑𝐶𝐵)
2019anim1i 615 . . . . . 6 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → (𝐶𝐵 ∧ (𝐹𝐶) ≠ ∅))
214, 5, 6cantnfs 9703 . . . . . . . . . . 11 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
228, 21mpbid 232 . . . . . . . . . 10 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
2322simpld 494 . . . . . . . . 9 (𝜑𝐹:𝐵𝐴)
2423adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐹:𝐵𝐴)
2524ffnd 6737 . . . . . . 7 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐹 Fn 𝐵)
266adantr 480 . . . . . . 7 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐵 ∈ On)
27 0ex 5312 . . . . . . . 8 ∅ ∈ V
2827a1i 11 . . . . . . 7 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ∅ ∈ V)
29 elsuppfn 8193 . . . . . . 7 ((𝐹 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝐶 ∈ (𝐹 supp ∅) ↔ (𝐶𝐵 ∧ (𝐹𝐶) ≠ ∅)))
3025, 26, 28, 29syl3anc 1370 . . . . . 6 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → (𝐶 ∈ (𝐹 supp ∅) ↔ (𝐶𝐵 ∧ (𝐹𝐶) ≠ ∅)))
3120, 30mpbird 257 . . . . 5 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → 𝐶 ∈ (𝐹 supp ∅))
3218, 31ffvelcdmd 7104 . . . 4 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → (𝐺𝐶) ∈ dom 𝐺)
339simprd 495 . . . . . 6 (𝜑 → dom 𝐺 ∈ ω)
3433adantr 480 . . . . 5 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → dom 𝐺 ∈ ω)
35 eqimss 4053 . . . . . . . . . 10 (𝑥 = dom 𝐺𝑥 ⊆ dom 𝐺)
3635biantrurd 532 . . . . . . . . 9 (𝑥 = dom 𝐺 → ((𝐺𝐶) ∈ 𝑥 ↔ (𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥)))
37 eleq2 2827 . . . . . . . . 9 (𝑥 = dom 𝐺 → ((𝐺𝐶) ∈ 𝑥 ↔ (𝐺𝐶) ∈ dom 𝐺))
3836, 37bitr3d 281 . . . . . . . 8 (𝑥 = dom 𝐺 → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) ↔ (𝐺𝐶) ∈ dom 𝐺))
39 fveq2 6906 . . . . . . . . 9 (𝑥 = dom 𝐺 → (𝐻𝑥) = (𝐻‘dom 𝐺))
4039sseq2d 4027 . . . . . . . 8 (𝑥 = dom 𝐺 → (((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑥) ↔ ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺)))
4138, 40imbi12d 344 . . . . . . 7 (𝑥 = dom 𝐺 → (((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑥)) ↔ ((𝐺𝐶) ∈ dom 𝐺 → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺))))
4241imbi2d 340 . . . . . 6 (𝑥 = dom 𝐺 → (((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑥))) ↔ ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐺𝐶) ∈ dom 𝐺 → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺)))))
43 sseq1 4020 . . . . . . . . 9 (𝑥 = ∅ → (𝑥 ⊆ dom 𝐺 ↔ ∅ ⊆ dom 𝐺))
44 eleq2 2827 . . . . . . . . 9 (𝑥 = ∅ → ((𝐺𝐶) ∈ 𝑥 ↔ (𝐺𝐶) ∈ ∅))
4543, 44anbi12d 632 . . . . . . . 8 (𝑥 = ∅ → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) ↔ (∅ ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ ∅)))
46 fveq2 6906 . . . . . . . . 9 (𝑥 = ∅ → (𝐻𝑥) = (𝐻‘∅))
4746sseq2d 4027 . . . . . . . 8 (𝑥 = ∅ → (((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑥) ↔ ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘∅)))
4845, 47imbi12d 344 . . . . . . 7 (𝑥 = ∅ → (((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑥)) ↔ ((∅ ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ ∅) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘∅))))
49 sseq1 4020 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥 ⊆ dom 𝐺𝑦 ⊆ dom 𝐺))
50 eleq2 2827 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝐺𝐶) ∈ 𝑥 ↔ (𝐺𝐶) ∈ 𝑦))
5149, 50anbi12d 632 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) ↔ (𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)))
52 fveq2 6906 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
5352sseq2d 4027 . . . . . . . 8 (𝑥 = 𝑦 → (((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑥) ↔ ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)))
5451, 53imbi12d 344 . . . . . . 7 (𝑥 = 𝑦 → (((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑥)) ↔ ((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦))))
55 sseq1 4020 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝑥 ⊆ dom 𝐺 ↔ suc 𝑦 ⊆ dom 𝐺))
56 eleq2 2827 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝐺𝐶) ∈ 𝑥 ↔ (𝐺𝐶) ∈ suc 𝑦))
5755, 56anbi12d 632 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) ↔ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ suc 𝑦)))
58 fveq2 6906 . . . . . . . . 9 (𝑥 = suc 𝑦 → (𝐻𝑥) = (𝐻‘suc 𝑦))
5958sseq2d 4027 . . . . . . . 8 (𝑥 = suc 𝑦 → (((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑥) ↔ ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
6057, 59imbi12d 344 . . . . . . 7 (𝑥 = suc 𝑦 → (((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑥)) ↔ ((suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ suc 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
61 noel 4343 . . . . . . . . . 10 ¬ (𝐺𝐶) ∈ ∅
6261pm2.21i 119 . . . . . . . . 9 ((𝐺𝐶) ∈ ∅ → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘∅))
6362adantl 481 . . . . . . . 8 ((∅ ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ ∅) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘∅))
6463a1i 11 . . . . . . 7 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((∅ ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ ∅) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘∅)))
65 fvex 6919 . . . . . . . . . . . 12 (𝐺𝐶) ∈ V
6665elsuc 6455 . . . . . . . . . . 11 ((𝐺𝐶) ∈ suc 𝑦 ↔ ((𝐺𝐶) ∈ 𝑦 ∨ (𝐺𝐶) = 𝑦))
67 sssucid 6465 . . . . . . . . . . . . . . . . 17 𝑦 ⊆ suc 𝑦
68 sstr 4003 . . . . . . . . . . . . . . . . 17 ((𝑦 ⊆ suc 𝑦 ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ⊆ dom 𝐺)
6967, 68mpan 690 . . . . . . . . . . . . . . . 16 (suc 𝑦 ⊆ dom 𝐺𝑦 ⊆ dom 𝐺)
7069ad2antrl 728 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)) → 𝑦 ⊆ dom 𝐺)
71 simprr 773 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)) → (𝐺𝐶) ∈ 𝑦)
72 pm2.27 42 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)))
7370, 71, 72syl2anc 584 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)))
74 cantnfval.h . . . . . . . . . . . . . . . . . . . . 21 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘))) +o 𝑧)), ∅)
7574cantnfvalf 9702 . . . . . . . . . . . . . . . . . . . 20 𝐻:ω⟶On
7675ffvelcdmi 7102 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ω → (𝐻𝑦) ∈ On)
7776ad2antlr 727 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻𝑦) ∈ On)
785ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐴 ∈ On)
796ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐵 ∈ On)
80 suppssdm 8200 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹 supp ∅) ⊆ dom 𝐹
8180, 23fssdm 6755 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
8281ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹 supp ∅) ⊆ 𝐵)
83 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → suc 𝑦 ⊆ dom 𝐺)
84 sucidg 6466 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ω → 𝑦 ∈ suc 𝑦)
8584ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ∈ suc 𝑦)
8683, 85sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ∈ dom 𝐺)
877oif 9567 . . . . . . . . . . . . . . . . . . . . . . . 24 𝐺:dom 𝐺⟶(𝐹 supp ∅)
8887ffvelcdmi 7102 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ dom 𝐺 → (𝐺𝑦) ∈ (𝐹 supp ∅))
8986, 88syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺𝑦) ∈ (𝐹 supp ∅))
9082, 89sseldd 3995 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺𝑦) ∈ 𝐵)
91 onelon 6410 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵 ∈ On ∧ (𝐺𝑦) ∈ 𝐵) → (𝐺𝑦) ∈ On)
9279, 90, 91syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺𝑦) ∈ On)
93 oecl 8573 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ (𝐺𝑦) ∈ On) → (𝐴o (𝐺𝑦)) ∈ On)
9478, 92, 93syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐴o (𝐺𝑦)) ∈ On)
9523ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐹:𝐵𝐴)
9695, 90ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹‘(𝐺𝑦)) ∈ 𝐴)
97 onelon 6410 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ On ∧ (𝐹‘(𝐺𝑦)) ∈ 𝐴) → (𝐹‘(𝐺𝑦)) ∈ On)
9878, 96, 97syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹‘(𝐺𝑦)) ∈ On)
99 omcl 8572 . . . . . . . . . . . . . . . . . . 19 (((𝐴o (𝐺𝑦)) ∈ On ∧ (𝐹‘(𝐺𝑦)) ∈ On) → ((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) ∈ On)
10094, 98, 99syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) ∈ On)
101 oaword2 8589 . . . . . . . . . . . . . . . . . 18 (((𝐻𝑦) ∈ On ∧ ((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) ∈ On) → (𝐻𝑦) ⊆ (((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) +o (𝐻𝑦)))
10277, 100, 101syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻𝑦) ⊆ (((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) +o (𝐻𝑦)))
1034, 5, 6, 7, 8, 74cantnfsuc 9707 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) +o (𝐻𝑦)))
104103ad4ant13 751 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻‘suc 𝑦) = (((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) +o (𝐻𝑦)))
105102, 104sseqtrrd 4036 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻𝑦) ⊆ (𝐻‘suc 𝑦))
106 sstr 4003 . . . . . . . . . . . . . . . . 17 ((((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦) ∧ (𝐻𝑦) ⊆ (𝐻‘suc 𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))
107106expcom 413 . . . . . . . . . . . . . . . 16 ((𝐻𝑦) ⊆ (𝐻‘suc 𝑦) → (((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
108105, 107syl 17 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
109108adantrr 717 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)) → (((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
11073, 109syld 47 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦)) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
111110expr 456 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐺𝐶) ∈ 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
112 simprr 773 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐺𝐶) = 𝑦)
113112fveq2d 6910 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐺‘(𝐺𝐶)) = (𝐺𝑦))
114 f1ocnvfv2 7296 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺:dom 𝐺1-1-onto→(𝐹 supp ∅) ∧ 𝐶 ∈ (𝐹 supp ∅)) → (𝐺‘(𝐺𝐶)) = 𝐶)
11515, 31, 114syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → (𝐺‘(𝐺𝐶)) = 𝐶)
116115ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐺‘(𝐺𝐶)) = 𝐶)
117113, 116eqtr3d 2776 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐺𝑦) = 𝐶)
118117oveq2d 7446 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐴o (𝐺𝑦)) = (𝐴o 𝐶))
119117fveq2d 6910 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐹‘(𝐺𝑦)) = (𝐹𝐶))
120118, 119oveq12d 7448 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → ((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) = ((𝐴o 𝐶) ·o (𝐹𝐶)))
121 oaword1 8588 . . . . . . . . . . . . . . . . . 18 ((((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) ∈ On ∧ (𝐻𝑦) ∈ On) → ((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) ⊆ (((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) +o (𝐻𝑦)))
122100, 77, 121syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) ⊆ (((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) +o (𝐻𝑦)))
123122adantrr 717 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → ((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) ⊆ (((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) +o (𝐻𝑦)))
124120, 123eqsstrrd 4034 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) +o (𝐻𝑦)))
125103ad4ant13 751 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → (𝐻‘suc 𝑦) = (((𝐴o (𝐺𝑦)) ·o (𝐹‘(𝐺𝑦))) +o (𝐻𝑦)))
126124, 125sseqtrrd 4036 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) = 𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))
127126expr 456 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐺𝐶) = 𝑦 → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))
128127a1dd 50 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐺𝐶) = 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
129111, 128jaod 859 . . . . . . . . . . 11 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (((𝐺𝐶) ∈ 𝑦 ∨ (𝐺𝐶) = 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
13066, 129biimtrid 242 . . . . . . . . . 10 ((((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐺𝐶) ∈ suc 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
131130expimpd 453 . . . . . . . . 9 (((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ suc 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
132131com23 86 . . . . . . . 8 (((𝜑 ∧ (𝐹𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ suc 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦))))
133132expcom 413 . . . . . . 7 (𝑦 ∈ ω → ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → (((𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑦)) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ suc 𝑦) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘suc 𝑦)))))
13448, 54, 60, 64, 133finds2 7920 . . . . . 6 (𝑥 ∈ ω → ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝑥 ⊆ dom 𝐺 ∧ (𝐺𝐶) ∈ 𝑥) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻𝑥))))
13542, 134vtoclga 3576 . . . . 5 (dom 𝐺 ∈ ω → ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐺𝐶) ∈ dom 𝐺 → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺))))
13634, 135mpcom 38 . . . 4 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐺𝐶) ∈ dom 𝐺 → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺)))
13732, 136mpd 15 . . 3 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ (𝐻‘dom 𝐺))
1384, 5, 6, 7, 8, 74cantnfval 9705 . . . 4 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺))
139138adantr 480 . . 3 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺))
140137, 139sseqtrrd 4036 . 2 ((𝜑 ∧ (𝐹𝐶) ≠ ∅) → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹))
141 onelon 6410 . . . . . 6 ((𝐵 ∈ On ∧ 𝐶𝐵) → 𝐶 ∈ On)
1426, 19, 141syl2anc 584 . . . . 5 (𝜑𝐶 ∈ On)
143 oecl 8573 . . . . 5 ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴o 𝐶) ∈ On)
1445, 142, 143syl2anc 584 . . . 4 (𝜑 → (𝐴o 𝐶) ∈ On)
145 om0 8553 . . . 4 ((𝐴o 𝐶) ∈ On → ((𝐴o 𝐶) ·o ∅) = ∅)
146144, 145syl 17 . . 3 (𝜑 → ((𝐴o 𝐶) ·o ∅) = ∅)
147 0ss 4405 . . 3 ∅ ⊆ ((𝐴 CNF 𝐵)‘𝐹)
148146, 147eqsstrdi 4049 . 2 (𝜑 → ((𝐴o 𝐶) ·o ∅) ⊆ ((𝐴 CNF 𝐵)‘𝐹))
1492, 140, 148pm2.61ne 3024 1 (𝜑 → ((𝐴o 𝐶) ·o (𝐹𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847   = wceq 1536  wcel 2105  wne 2937  Vcvv 3477  wss 3962  c0 4338   class class class wbr 5147   E cep 5587   We wwe 5639  ccnv 5687  dom cdm 5688  Oncon0 6385  suc csuc 6387   Fn wfn 6557  wf 6558  1-1-ontowf1o 6561  cfv 6562   Isom wiso 6563  (class class class)co 7430  cmpo 7432  ωcom 7886   supp csupp 8183  seqωcseqom 8485   +o coa 8501   ·o comu 8502  o coe 8503   finSupp cfsupp 9398  OrdIsocoi 9546   CNF ccnf 9698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-seqom 8486  df-1o 8504  df-oadd 8508  df-omul 8509  df-oexp 8510  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-oi 9547  df-cnf 9699
This theorem is referenced by:  cantnflem3  9728
  Copyright terms: Public domain W3C validator