| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . 3
⊢ ((𝐹‘𝐶) = ∅ → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) = ((𝐴 ↑o 𝐶) ·o
∅)) |
| 2 | 1 | sseq1d 4015 |
. 2
⊢ ((𝐹‘𝐶) = ∅ → (((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹) ↔ ((𝐴 ↑o 𝐶) ·o ∅) ⊆
((𝐴 CNF 𝐵)‘𝐹))) |
| 3 | | ovexd 7466 |
. . . . . . . . 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
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
| 9 | 4, 5, 6, 7, 8 | cantnfcl 9707 |
. . . . . . . . . 10
⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω)) |
| 10 | 9 | simpld 494 |
. . . . . . . . 9
⊢ (𝜑 → E We (𝐹 supp ∅)) |
| 11 | 7 | oiiso 9577 |
. . . . . . . . 9
⊢ (((𝐹 supp ∅) ∈ V ∧ E
We (𝐹 supp ∅)) →
𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅))) |
| 12 | 3, 10, 11 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅))) |
| 13 | | isof1o 7343 |
. . . . . . . 8
⊢ (𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) → 𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅)) |
| 14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅)) |
| 15 | 14 | adantr 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 𝐺) |
| 18 | 15, 16, 17 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺) |
| 19 | | cantnfle.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝐵) |
| 20 | 19 | anim1i 615 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → (𝐶 ∈ 𝐵 ∧ (𝐹‘𝐶) ≠ ∅)) |
| 21 | 4, 5, 6 | cantnfs 9706 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) |
| 22 | 8, 21 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)) |
| 23 | 22 | simpld 494 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐵⟶𝐴) |
| 24 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → 𝐹:𝐵⟶𝐴) |
| 25 | 24 | ffnd 6737 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → 𝐹 Fn 𝐵) |
| 26 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → 𝐵 ∈ On) |
| 27 | | 0ex 5307 |
. . . . . . . 8
⊢ ∅
∈ V |
| 28 | 27 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ∅ ∈
V) |
| 29 | | elsuppfn 8195 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(𝐶 ∈ (𝐹 supp ∅) ↔ (𝐶 ∈ 𝐵 ∧ (𝐹‘𝐶) ≠ ∅))) |
| 30 | 25, 26, 28, 29 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → (𝐶 ∈ (𝐹 supp ∅) ↔ (𝐶 ∈ 𝐵 ∧ (𝐹‘𝐶) ≠ ∅))) |
| 31 | 20, 30 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → 𝐶 ∈ (𝐹 supp ∅)) |
| 32 | 18, 31 | ffvelcdmd 7105 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → (◡𝐺‘𝐶) ∈ dom 𝐺) |
| 33 | 9 | simprd 495 |
. . . . . 6
⊢ (𝜑 → dom 𝐺 ∈ ω) |
| 34 | 33 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → dom 𝐺 ∈ ω) |
| 35 | | eqimss 4042 |
. . . . . . . . . 10
⊢ (𝑥 = dom 𝐺 → 𝑥 ⊆ dom 𝐺) |
| 36 | 35 | biantrurd 532 |
. . . . . . . . 9
⊢ (𝑥 = dom 𝐺 → ((◡𝐺‘𝐶) ∈ 𝑥 ↔ (𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥))) |
| 37 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑥 = dom 𝐺 → ((◡𝐺‘𝐶) ∈ 𝑥 ↔ (◡𝐺‘𝐶) ∈ dom 𝐺)) |
| 38 | 36, 37 | bitr3d 281 |
. . . . . . . 8
⊢ (𝑥 = dom 𝐺 → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) ↔ (◡𝐺‘𝐶) ∈ dom 𝐺)) |
| 39 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = dom 𝐺 → (𝐻‘𝑥) = (𝐻‘dom 𝐺)) |
| 40 | 39 | sseq2d 4016 |
. . . . . . . 8
⊢ (𝑥 = dom 𝐺 → (((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑥) ↔ ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺))) |
| 41 | 38, 40 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = dom 𝐺 → (((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑥)) ↔ ((◡𝐺‘𝐶) ∈ dom 𝐺 → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺)))) |
| 42 | 41 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = dom 𝐺 → (((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑥))) ↔ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((◡𝐺‘𝐶) ∈ dom 𝐺 → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺))))) |
| 43 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑥 ⊆ dom 𝐺 ↔ ∅ ⊆ dom 𝐺)) |
| 44 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → ((◡𝐺‘𝐶) ∈ 𝑥 ↔ (◡𝐺‘𝐶) ∈ ∅)) |
| 45 | 43, 44 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) ↔ (∅ ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ ∅))) |
| 46 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝐻‘𝑥) = (𝐻‘∅)) |
| 47 | 46 | sseq2d 4016 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑥) ↔ ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘∅))) |
| 48 | 45, 47 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = ∅ → (((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑥)) ↔ ((∅ ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ ∅) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘∅)))) |
| 49 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ dom 𝐺 ↔ 𝑦 ⊆ dom 𝐺)) |
| 50 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((◡𝐺‘𝐶) ∈ 𝑥 ↔ (◡𝐺‘𝐶) ∈ 𝑦)) |
| 51 | 49, 50 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) ↔ (𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦))) |
| 52 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) |
| 53 | 52 | sseq2d 4016 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑥) ↔ ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦))) |
| 54 | 51, 53 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑥)) ↔ ((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)))) |
| 55 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (𝑥 ⊆ dom 𝐺 ↔ suc 𝑦 ⊆ dom 𝐺)) |
| 56 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → ((◡𝐺‘𝐶) ∈ 𝑥 ↔ (◡𝐺‘𝐶) ∈ suc 𝑦)) |
| 57 | 55, 56 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) ↔ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ suc 𝑦))) |
| 58 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (𝐻‘𝑥) = (𝐻‘suc 𝑦)) |
| 59 | 58 | sseq2d 4016 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → (((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑥) ↔ ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
| 60 | 57, 59 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑥)) ↔ ((suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ suc 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
| 61 | | noel 4338 |
. . . . . . . . . 10
⊢ ¬
(◡𝐺‘𝐶) ∈ ∅ |
| 62 | 61 | pm2.21i 119 |
. . . . . . . . 9
⊢ ((◡𝐺‘𝐶) ∈ ∅ → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘∅)) |
| 63 | 62 | adantl 481 |
. . . . . . . 8
⊢ ((∅
⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ ∅) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘∅)) |
| 64 | 63 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((∅ ⊆ dom
𝐺 ∧ (◡𝐺‘𝐶) ∈ ∅) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘∅))) |
| 65 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (◡𝐺‘𝐶) ∈ V |
| 66 | 65 | elsuc 6454 |
. . . . . . . . . . 11
⊢ ((◡𝐺‘𝐶) ∈ suc 𝑦 ↔ ((◡𝐺‘𝐶) ∈ 𝑦 ∨ (◡𝐺‘𝐶) = 𝑦)) |
| 67 | | sssucid 6464 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ⊆ suc 𝑦 |
| 68 | | sstr 3992 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ suc 𝑦 ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ⊆ dom 𝐺) |
| 69 | 67, 68 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑦 ⊆ dom 𝐺 → 𝑦 ⊆ dom 𝐺) |
| 70 | 69 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦)) → 𝑦 ⊆ dom 𝐺) |
| 71 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦)) → (◡𝐺‘𝐶) ∈ 𝑦) |
| 72 | | pm2.27 42 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦))) |
| 73 | 70, 71, 72 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦)) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦))) |
| 74 | | cantnfval.h |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅) |
| 75 | 74 | cantnfvalf 9705 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐻:ω⟶On |
| 76 | 75 | ffvelcdmi 7103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ω → (𝐻‘𝑦) ∈ On) |
| 77 | 76 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻‘𝑦) ∈ On) |
| 78 | 5 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐴 ∈ On) |
| 79 | 6 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐵 ∈ On) |
| 80 | | suppssdm 8202 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹 supp ∅) ⊆ dom 𝐹 |
| 81 | 80, 23 | fssdm 6755 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐵) |
| 82 | 81 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹 supp ∅) ⊆ 𝐵) |
| 83 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → suc 𝑦 ⊆ dom 𝐺) |
| 84 | | sucidg 6465 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ω → 𝑦 ∈ suc 𝑦) |
| 85 | 84 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ∈ suc 𝑦) |
| 86 | 83, 85 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ∈ dom 𝐺) |
| 87 | 7 | oif 9570 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅) |
| 88 | 87 | ffvelcdmi 7103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ dom 𝐺 → (𝐺‘𝑦) ∈ (𝐹 supp ∅)) |
| 89 | 86, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺‘𝑦) ∈ (𝐹 supp ∅)) |
| 90 | 82, 89 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺‘𝑦) ∈ 𝐵) |
| 91 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈ On ∧ (𝐺‘𝑦) ∈ 𝐵) → (𝐺‘𝑦) ∈ On) |
| 92 | 79, 90, 91 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺‘𝑦) ∈ On) |
| 93 | | oecl 8575 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ (𝐺‘𝑦) ∈ On) → (𝐴 ↑o (𝐺‘𝑦)) ∈ On) |
| 94 | 78, 92, 93 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐴 ↑o (𝐺‘𝑦)) ∈ On) |
| 95 | 23 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐹:𝐵⟶𝐴) |
| 96 | 95, 90 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹‘(𝐺‘𝑦)) ∈ 𝐴) |
| 97 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘𝑦)) ∈ On) |
| 98 | 78, 96, 97 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹‘(𝐺‘𝑦)) ∈ On) |
| 99 | | omcl 8574 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ↑o (𝐺‘𝑦)) ∈ On ∧ (𝐹‘(𝐺‘𝑦)) ∈ On) → ((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ∈ On) |
| 100 | 94, 98, 99 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ∈ On) |
| 101 | | oaword2 8591 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐻‘𝑦) ∈ On ∧ ((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ∈ On) → (𝐻‘𝑦) ⊆ (((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) +o (𝐻‘𝑦))) |
| 102 | 77, 100, 101 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻‘𝑦) ⊆ (((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) +o (𝐻‘𝑦))) |
| 103 | 4, 5, 6, 7, 8, 74 | cantnfsuc 9710 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) +o (𝐻‘𝑦))) |
| 104 | 103 | ad4ant13 751 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻‘suc 𝑦) = (((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) +o (𝐻‘𝑦))) |
| 105 | 102, 104 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻‘𝑦) ⊆ (𝐻‘suc 𝑦)) |
| 106 | | sstr 3992 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦) ∧ (𝐻‘𝑦) ⊆ (𝐻‘suc 𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)) |
| 107 | 106 | expcom 413 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻‘𝑦) ⊆ (𝐻‘suc 𝑦) → (((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
| 108 | 105, 107 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
| 109 | 108 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦)) → (((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
| 110 | 73, 109 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦)) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
| 111 | 110 | expr 456 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((◡𝐺‘𝐶) ∈ 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
| 112 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (◡𝐺‘𝐶) = 𝑦) |
| 113 | 112 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐺‘(◡𝐺‘𝐶)) = (𝐺‘𝑦)) |
| 114 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) ∧ 𝐶 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝐶)) = 𝐶) |
| 115 | 15, 31, 114 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → (𝐺‘(◡𝐺‘𝐶)) = 𝐶) |
| 116 | 115 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐺‘(◡𝐺‘𝐶)) = 𝐶) |
| 117 | 113, 116 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐺‘𝑦) = 𝐶) |
| 118 | 117 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐴 ↑o (𝐺‘𝑦)) = (𝐴 ↑o 𝐶)) |
| 119 | 117 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐹‘(𝐺‘𝑦)) = (𝐹‘𝐶)) |
| 120 | 118, 119 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → ((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) = ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶))) |
| 121 | | oaword1 8590 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ∈ On ∧ (𝐻‘𝑦) ∈ On) → ((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ⊆ (((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) +o (𝐻‘𝑦))) |
| 122 | 100, 77, 121 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ⊆ (((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) +o (𝐻‘𝑦))) |
| 123 | 122 | adantrr 717 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → ((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ⊆ (((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) +o (𝐻‘𝑦))) |
| 124 | 120, 123 | eqsstrrd 4019 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) +o (𝐻‘𝑦))) |
| 125 | 103 | ad4ant13 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐻‘suc 𝑦) = (((𝐴 ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) +o (𝐻‘𝑦))) |
| 126 | 124, 125 | sseqtrrd 4021 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)) |
| 127 | 126 | expr 456 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((◡𝐺‘𝐶) = 𝑦 → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
| 128 | 127 | a1dd 50 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((◡𝐺‘𝐶) = 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
| 129 | 111, 128 | jaod 860 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (((◡𝐺‘𝐶) ∈ 𝑦 ∨ (◡𝐺‘𝐶) = 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
| 130 | 66, 129 | biimtrid 242 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((◡𝐺‘𝐶) ∈ suc 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
| 131 | 130 | expimpd 453 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ suc 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
| 132 | 131 | com23 86 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ suc 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
| 133 | 132 | expcom 413 |
. . . . . . 7
⊢ (𝑦 ∈ ω → ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ suc 𝑦) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))))) |
| 134 | 48, 54, 60, 64, 133 | finds2 7920 |
. . . . . 6
⊢ (𝑥 ∈ ω → ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘𝑥)))) |
| 135 | 42, 134 | vtoclga 3577 |
. . . . 5
⊢ (dom
𝐺 ∈ ω →
((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((◡𝐺‘𝐶) ∈ dom 𝐺 → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺)))) |
| 136 | 34, 135 | mpcom 38 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((◡𝐺‘𝐶) ∈ dom 𝐺 → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺))) |
| 137 | 32, 136 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺)) |
| 138 | 4, 5, 6, 7, 8, 74 | cantnfval 9708 |
. . . 4
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺)) |
| 139 | 138 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺)) |
| 140 | 137, 139 | sseqtrrd 4021 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹)) |
| 141 | | onelon 6409 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ On) |
| 142 | 6, 19, 141 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ On) |
| 143 | | oecl 8575 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On) |
| 144 | 5, 142, 143 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐴 ↑o 𝐶) ∈ On) |
| 145 | | om0 8555 |
. . . 4
⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) ·o ∅)
= ∅) |
| 146 | 144, 145 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐴 ↑o 𝐶) ·o ∅) =
∅) |
| 147 | | 0ss 4400 |
. . 3
⊢ ∅
⊆ ((𝐴 CNF 𝐵)‘𝐹) |
| 148 | 146, 147 | eqsstrdi 4028 |
. 2
⊢ (𝜑 → ((𝐴 ↑o 𝐶) ·o ∅) ⊆
((𝐴 CNF 𝐵)‘𝐹)) |
| 149 | 2, 140, 148 | pm2.61ne 3027 |
1
⊢ (𝜑 → ((𝐴 ↑o 𝐶) ·o (𝐹‘𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹)) |