Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . 3
⊢ ((𝐹‘𝐶) = ∅ → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) = ((𝐴 ↑𝑜 𝐶) ·𝑜
∅)) |
2 | 1 | sseq1d 3595 |
. 2
⊢ ((𝐹‘𝐶) = ∅ → (((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹) ↔ ((𝐴 ↑𝑜 𝐶) ·𝑜
∅) ⊆ ((𝐴 CNF
𝐵)‘𝐹))) |
3 | | cantnfs.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ On) |
4 | | suppssdm 7195 |
. . . . . . . . . . 11
⊢ (𝐹 supp ∅) ⊆ dom 𝐹 |
5 | | cantnfcl.f |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
6 | | cantnfs.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
7 | | cantnfs.a |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ On) |
8 | 6, 7, 3 | cantnfs 8446 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) |
9 | 5, 8 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)) |
10 | 9 | simpld 474 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐵⟶𝐴) |
11 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐵⟶𝐴 → dom 𝐹 = 𝐵) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = 𝐵) |
13 | 4, 12 | syl5sseq 3616 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐵) |
14 | 3, 13 | ssexd 4733 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 supp ∅) ∈ V) |
15 | | cantnfcl.g |
. . . . . . . . . . 11
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
16 | 6, 7, 3, 15, 5 | cantnfcl 8447 |
. . . . . . . . . 10
⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω)) |
17 | 16 | simpld 474 |
. . . . . . . . 9
⊢ (𝜑 → E We (𝐹 supp ∅)) |
18 | 15 | oiiso 8325 |
. . . . . . . . 9
⊢ (((𝐹 supp ∅) ∈ V ∧ E
We (𝐹 supp ∅)) →
𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅))) |
19 | 14, 17, 18 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅))) |
20 | | isof1o 6473 |
. . . . . . . 8
⊢ (𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) → 𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅)) |
21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅)) |
22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → 𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅)) |
23 | | f1ocnv 6062 |
. . . . . 6
⊢ (𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) → ◡𝐺:(𝐹 supp ∅)–1-1-onto→dom
𝐺) |
24 | | f1of 6050 |
. . . . . 6
⊢ (◡𝐺:(𝐹 supp ∅)–1-1-onto→dom
𝐺 → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺) |
25 | 22, 23, 24 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ◡𝐺:(𝐹 supp ∅)⟶dom 𝐺) |
26 | | cantnfle.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝐵) |
27 | 26 | anim1i 590 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → (𝐶 ∈ 𝐵 ∧ (𝐹‘𝐶) ≠ ∅)) |
28 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → 𝐹:𝐵⟶𝐴) |
29 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:𝐵⟶𝐴 → 𝐹 Fn 𝐵) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → 𝐹 Fn 𝐵) |
31 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → 𝐵 ∈ On) |
32 | | 0ex 4718 |
. . . . . . . 8
⊢ ∅
∈ V |
33 | 32 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ∅ ∈
V) |
34 | | elsuppfn 7190 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(𝐶 ∈ (𝐹 supp ∅) ↔ (𝐶 ∈ 𝐵 ∧ (𝐹‘𝐶) ≠ ∅))) |
35 | 30, 31, 33, 34 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → (𝐶 ∈ (𝐹 supp ∅) ↔ (𝐶 ∈ 𝐵 ∧ (𝐹‘𝐶) ≠ ∅))) |
36 | 27, 35 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → 𝐶 ∈ (𝐹 supp ∅)) |
37 | 25, 36 | ffvelrnd 6268 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → (◡𝐺‘𝐶) ∈ dom 𝐺) |
38 | 16 | simprd 478 |
. . . . . 6
⊢ (𝜑 → dom 𝐺 ∈ ω) |
39 | 38 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → dom 𝐺 ∈ ω) |
40 | | eqimss 3620 |
. . . . . . . . . 10
⊢ (𝑥 = dom 𝐺 → 𝑥 ⊆ dom 𝐺) |
41 | 40 | biantrurd 528 |
. . . . . . . . 9
⊢ (𝑥 = dom 𝐺 → ((◡𝐺‘𝐶) ∈ 𝑥 ↔ (𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥))) |
42 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑥 = dom 𝐺 → ((◡𝐺‘𝐶) ∈ 𝑥 ↔ (◡𝐺‘𝐶) ∈ dom 𝐺)) |
43 | 41, 42 | bitr3d 269 |
. . . . . . . 8
⊢ (𝑥 = dom 𝐺 → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) ↔ (◡𝐺‘𝐶) ∈ dom 𝐺)) |
44 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = dom 𝐺 → (𝐻‘𝑥) = (𝐻‘dom 𝐺)) |
45 | 44 | sseq2d 3596 |
. . . . . . . 8
⊢ (𝑥 = dom 𝐺 → (((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑥) ↔ ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺))) |
46 | 43, 45 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = dom 𝐺 → (((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑥)) ↔ ((◡𝐺‘𝐶) ∈ dom 𝐺 → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺)))) |
47 | 46 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = dom 𝐺 → (((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑥))) ↔ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((◡𝐺‘𝐶) ∈ dom 𝐺 → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺))))) |
48 | | sseq1 3589 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑥 ⊆ dom 𝐺 ↔ ∅ ⊆ dom 𝐺)) |
49 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → ((◡𝐺‘𝐶) ∈ 𝑥 ↔ (◡𝐺‘𝐶) ∈ ∅)) |
50 | 48, 49 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) ↔ (∅ ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ ∅))) |
51 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝐻‘𝑥) = (𝐻‘∅)) |
52 | 51 | sseq2d 3596 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (((𝐴 ↑𝑜
𝐶)
·𝑜 (𝐹‘𝐶)) ⊆ (𝐻‘𝑥) ↔ ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘∅))) |
53 | 50, 52 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = ∅ → (((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑥)) ↔ ((∅ ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ ∅) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘∅)))) |
54 | | sseq1 3589 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ dom 𝐺 ↔ 𝑦 ⊆ dom 𝐺)) |
55 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((◡𝐺‘𝐶) ∈ 𝑥 ↔ (◡𝐺‘𝐶) ∈ 𝑦)) |
56 | 54, 55 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) ↔ (𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦))) |
57 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) |
58 | 57 | sseq2d 3596 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑥) ↔ ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦))) |
59 | 56, 58 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑥)) ↔ ((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)))) |
60 | | sseq1 3589 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (𝑥 ⊆ dom 𝐺 ↔ suc 𝑦 ⊆ dom 𝐺)) |
61 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → ((◡𝐺‘𝐶) ∈ 𝑥 ↔ (◡𝐺‘𝐶) ∈ suc 𝑦)) |
62 | 60, 61 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) ↔ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ suc 𝑦))) |
63 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (𝐻‘𝑥) = (𝐻‘suc 𝑦)) |
64 | 63 | sseq2d 3596 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → (((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑥) ↔ ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
65 | 62, 64 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑥)) ↔ ((suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ suc 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
66 | | noel 3878 |
. . . . . . . . . 10
⊢ ¬
(◡𝐺‘𝐶) ∈ ∅ |
67 | 66 | pm2.21i 115 |
. . . . . . . . 9
⊢ ((◡𝐺‘𝐶) ∈ ∅ → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘∅)) |
68 | 67 | adantl 481 |
. . . . . . . 8
⊢ ((∅
⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ ∅) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘∅)) |
69 | 68 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((∅ ⊆ dom
𝐺 ∧ (◡𝐺‘𝐶) ∈ ∅) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘∅))) |
70 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (◡𝐺‘𝐶) ∈ V |
71 | 70 | elsuc 5711 |
. . . . . . . . . . 11
⊢ ((◡𝐺‘𝐶) ∈ suc 𝑦 ↔ ((◡𝐺‘𝐶) ∈ 𝑦 ∨ (◡𝐺‘𝐶) = 𝑦)) |
72 | | sssucid 5719 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ⊆ suc 𝑦 |
73 | | sstr 3576 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ suc 𝑦 ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ⊆ dom 𝐺) |
74 | 72, 73 | mpan 702 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝑦 ⊆ dom 𝐺 → 𝑦 ⊆ dom 𝐺) |
75 | 74 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦)) → 𝑦 ⊆ dom 𝐺) |
76 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦)) → (◡𝐺‘𝐶) ∈ 𝑦) |
77 | | pm2.27 41 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦))) |
78 | 75, 76, 77 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦)) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦))) |
79 | | cantnfval.h |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐻 =
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑𝑜 (𝐺‘𝑘)) ·𝑜 (𝐹‘(𝐺‘𝑘))) +𝑜 𝑧)), ∅) |
80 | 79 | cantnfvalf 8445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐻:ω⟶On |
81 | 80 | ffvelrni 6266 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ω → (𝐻‘𝑦) ∈ On) |
82 | 81 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻‘𝑦) ∈ On) |
83 | 7 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐴 ∈ On) |
84 | 3 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐵 ∈ On) |
85 | 13 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹 supp ∅) ⊆ 𝐵) |
86 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → suc 𝑦 ⊆ dom 𝐺) |
87 | | sucidg 5720 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ω → 𝑦 ∈ suc 𝑦) |
88 | 87 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ∈ suc 𝑦) |
89 | 86, 88 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ∈ dom 𝐺) |
90 | 15 | oif 8318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅) |
91 | 90 | ffvelrni 6266 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ dom 𝐺 → (𝐺‘𝑦) ∈ (𝐹 supp ∅)) |
92 | 89, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺‘𝑦) ∈ (𝐹 supp ∅)) |
93 | 85, 92 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺‘𝑦) ∈ 𝐵) |
94 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈ On ∧ (𝐺‘𝑦) ∈ 𝐵) → (𝐺‘𝑦) ∈ On) |
95 | 84, 93, 94 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐺‘𝑦) ∈ On) |
96 | | oecl 7504 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ (𝐺‘𝑦) ∈ On) → (𝐴 ↑𝑜 (𝐺‘𝑦)) ∈ On) |
97 | 83, 95, 96 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐴 ↑𝑜 (𝐺‘𝑦)) ∈ On) |
98 | 10 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝐹:𝐵⟶𝐴) |
99 | 98, 93 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹‘(𝐺‘𝑦)) ∈ 𝐴) |
100 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝐺‘𝑦)) ∈ 𝐴) → (𝐹‘(𝐺‘𝑦)) ∈ On) |
101 | 83, 99, 100 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐹‘(𝐺‘𝑦)) ∈ On) |
102 | | omcl 7503 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ↑𝑜
(𝐺‘𝑦)) ∈ On ∧ (𝐹‘(𝐺‘𝑦)) ∈ On) → ((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) ∈ On) |
103 | 97, 101, 102 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) ∈ On) |
104 | | oaword2 7520 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐻‘𝑦) ∈ On ∧ ((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) ∈ On) → (𝐻‘𝑦) ⊆ (((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) +𝑜 (𝐻‘𝑦))) |
105 | 82, 103, 104 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻‘𝑦) ⊆ (((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) +𝑜 (𝐻‘𝑦))) |
106 | | simplll 794 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝜑) |
107 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → 𝑦 ∈ ω) |
108 | 6, 7, 3, 15, 5, 79 | cantnfsuc 8450 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) +𝑜 (𝐻‘𝑦))) |
109 | 106, 107,
108 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻‘suc 𝑦) = (((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) +𝑜 (𝐻‘𝑦))) |
110 | 105, 109 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (𝐻‘𝑦) ⊆ (𝐻‘suc 𝑦)) |
111 | | sstr 3576 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ↑𝑜
𝐶)
·𝑜 (𝐹‘𝐶)) ⊆ (𝐻‘𝑦) ∧ (𝐻‘𝑦) ⊆ (𝐻‘suc 𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)) |
112 | 111 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐻‘𝑦) ⊆ (𝐻‘suc 𝑦) → (((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
113 | 110, 112 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
114 | 113 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦)) → (((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
115 | 78, 114 | syld 46 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦)) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
116 | 115 | expr 641 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((◡𝐺‘𝐶) ∈ 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
117 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (◡𝐺‘𝐶) = 𝑦) |
118 | 117 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐺‘(◡𝐺‘𝐶)) = (𝐺‘𝑦)) |
119 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺:dom 𝐺–1-1-onto→(𝐹 supp ∅) ∧ 𝐶 ∈ (𝐹 supp ∅)) → (𝐺‘(◡𝐺‘𝐶)) = 𝐶) |
120 | 22, 36, 119 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → (𝐺‘(◡𝐺‘𝐶)) = 𝐶) |
121 | 120 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐺‘(◡𝐺‘𝐶)) = 𝐶) |
122 | 118, 121 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐺‘𝑦) = 𝐶) |
123 | 122 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐴 ↑𝑜 (𝐺‘𝑦)) = (𝐴 ↑𝑜 𝐶)) |
124 | 122 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐹‘(𝐺‘𝑦)) = (𝐹‘𝐶)) |
125 | 123, 124 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → ((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) = ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶))) |
126 | | oaword1 7519 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ↑𝑜
(𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) ∈ On ∧ (𝐻‘𝑦) ∈ On) → ((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) ⊆ (((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) +𝑜 (𝐻‘𝑦))) |
127 | 103, 82, 126 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) ⊆ (((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) +𝑜 (𝐻‘𝑦))) |
128 | 127 | adantrr 749 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → ((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) ⊆ (((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) +𝑜 (𝐻‘𝑦))) |
129 | 125, 128 | eqsstr3d 3603 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) +𝑜 (𝐻‘𝑦))) |
130 | 109 | adantrr 749 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → (𝐻‘suc 𝑦) = (((𝐴 ↑𝑜 (𝐺‘𝑦)) ·𝑜 (𝐹‘(𝐺‘𝑦))) +𝑜 (𝐻‘𝑦))) |
131 | 129, 130 | sseqtr4d 3605 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) = 𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)) |
132 | 131 | expr 641 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((◡𝐺‘𝐶) = 𝑦 → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))) |
133 | 132 | a1dd 48 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((◡𝐺‘𝐶) = 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
134 | 116, 133 | jaod 394 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → (((◡𝐺‘𝐶) ∈ 𝑦 ∨ (◡𝐺‘𝐶) = 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
135 | 71, 134 | syl5bi 231 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) ∧ suc 𝑦 ⊆ dom 𝐺) → ((◡𝐺‘𝐶) ∈ suc 𝑦 → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
136 | 135 | expimpd 627 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ suc 𝑦) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
137 | 136 | com23 84 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) ∧ 𝑦 ∈ ω) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ suc 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦)))) |
138 | 137 | expcom 450 |
. . . . . . 7
⊢ (𝑦 ∈ ω → ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → (((𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑦)) → ((suc 𝑦 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ suc 𝑦) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘suc 𝑦))))) |
139 | 53, 59, 65, 69, 138 | finds2 6986 |
. . . . . 6
⊢ (𝑥 ∈ ω → ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((𝑥 ⊆ dom 𝐺 ∧ (◡𝐺‘𝐶) ∈ 𝑥) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘𝑥)))) |
140 | 47, 139 | vtoclga 3245 |
. . . . 5
⊢ (dom
𝐺 ∈ ω →
((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((◡𝐺‘𝐶) ∈ dom 𝐺 → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺)))) |
141 | 39, 140 | mpcom 37 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((◡𝐺‘𝐶) ∈ dom 𝐺 → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺))) |
142 | 37, 141 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ (𝐻‘dom 𝐺)) |
143 | 6, 7, 3, 15, 5, 79 | cantnfval 8448 |
. . . 4
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺)) |
144 | 143 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺)) |
145 | 142, 144 | sseqtr4d 3605 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝐶) ≠ ∅) → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹)) |
146 | | onelon 5665 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ On) |
147 | 3, 26, 146 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ On) |
148 | | oecl 7504 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑𝑜
𝐶) ∈
On) |
149 | 7, 147, 148 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐴 ↑𝑜 𝐶) ∈ On) |
150 | | om0 7484 |
. . . 4
⊢ ((𝐴 ↑𝑜
𝐶) ∈ On → ((𝐴 ↑𝑜
𝐶)
·𝑜 ∅) = ∅) |
151 | 149, 150 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐴 ↑𝑜 𝐶) ·𝑜
∅) = ∅) |
152 | | 0ss 3924 |
. . 3
⊢ ∅
⊆ ((𝐴 CNF 𝐵)‘𝐹) |
153 | 151, 152 | syl6eqss 3618 |
. 2
⊢ (𝜑 → ((𝐴 ↑𝑜 𝐶) ·𝑜
∅) ⊆ ((𝐴 CNF
𝐵)‘𝐹)) |
154 | 2, 145, 153 | pm2.61ne 2867 |
1
⊢ (𝜑 → ((𝐴 ↑𝑜 𝐶) ·𝑜
(𝐹‘𝐶)) ⊆ ((𝐴 CNF 𝐵)‘𝐹)) |