Proof of Theorem cantnflem1d
Step | Hyp | Ref
| Expression |
1 | | cantnfs.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ On) |
2 | | cantnfs.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ On) |
3 | | cantnfs.s |
. . . . . . . . 9
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
4 | | oemapval.t |
. . . . . . . . 9
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
5 | | oemapval.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
6 | | oemapval.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ 𝑆) |
7 | | oemapvali.r |
. . . . . . . . 9
⊢ (𝜑 → 𝐹𝑇𝐺) |
8 | | oemapvali.x |
. . . . . . . . 9
⊢ 𝑋 = ∪
{𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} |
9 | 3, 1, 2, 4, 5, 6, 7, 8 | oemapvali 8464 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) |
10 | 9 | simp1d 1066 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
11 | | onelon 5665 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On) |
12 | 2, 10, 11 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ On) |
13 | | oecl 7504 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴 ↑𝑜
𝑋) ∈
On) |
14 | 1, 12, 13 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐴 ↑𝑜 𝑋) ∈ On) |
15 | 3, 1, 2 | cantnfs 8446 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) |
16 | 6, 15 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) |
17 | 16 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
18 | 17, 10 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴) |
19 | | onelon 5665 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (𝐺‘𝑋) ∈ 𝐴) → (𝐺‘𝑋) ∈ On) |
20 | 1, 18, 19 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝑋) ∈ On) |
21 | | omcl 7503 |
. . . . 5
⊢ (((𝐴 ↑𝑜
𝑋) ∈ On ∧ (𝐺‘𝑋) ∈ On) → ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)) ∈ On) |
22 | 14, 20, 21 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)) ∈ On) |
23 | | suppssdm 7195 |
. . . . . . . . . . . 12
⊢ (𝐺 supp ∅) ⊆ dom 𝐺 |
24 | | fdm 5964 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐵⟶𝐴 → dom 𝐺 = 𝐵) |
25 | 17, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → dom 𝐺 = 𝐵) |
26 | 23, 25 | syl5sseq 3616 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵) |
27 | 2, 26 | ssexd 4733 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 supp ∅) ∈ V) |
28 | | cantnflem1.o |
. . . . . . . . . . . 12
⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅)) |
29 | 3, 1, 2, 28, 6 | cantnfcl 8447 |
. . . . . . . . . . 11
⊢ (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω)) |
30 | 29 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → E We (𝐺 supp ∅)) |
31 | 28 | oiiso 8325 |
. . . . . . . . . 10
⊢ (((𝐺 supp ∅) ∈ V ∧ E
We (𝐺 supp ∅)) →
𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅))) |
32 | 27, 30, 31 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅))) |
33 | | isof1o 6473 |
. . . . . . . . 9
⊢ (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅)) |
34 | 32, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅)) |
35 | | f1ocnv 6062 |
. . . . . . . 8
⊢ (𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) → ◡𝑂:(𝐺 supp ∅)–1-1-onto→dom
𝑂) |
36 | | f1of 6050 |
. . . . . . . 8
⊢ (◡𝑂:(𝐺 supp ∅)–1-1-onto→dom
𝑂 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂) |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂) |
38 | 3, 1, 2, 4, 5, 6, 7, 8 | cantnflem1a 8465 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅)) |
39 | 37, 38 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (◡𝑂‘𝑋) ∈ dom 𝑂) |
40 | 29 | simprd 478 |
. . . . . 6
⊢ (𝜑 → dom 𝑂 ∈ ω) |
41 | | elnn 6967 |
. . . . . 6
⊢ (((◡𝑂‘𝑋) ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (◡𝑂‘𝑋) ∈ ω) |
42 | 39, 40, 41 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (◡𝑂‘𝑋) ∈ ω) |
43 | | cantnflem1.h |
. . . . . . 7
⊢ 𝐻 =
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑𝑜 (𝑂‘𝑘)) ·𝑜 (𝐺‘(𝑂‘𝑘))) +𝑜 𝑧)), ∅) |
44 | 43 | cantnfvalf 8445 |
. . . . . 6
⊢ 𝐻:ω⟶On |
45 | 44 | ffvelrni 6266 |
. . . . 5
⊢ ((◡𝑂‘𝑋) ∈ ω → (𝐻‘(◡𝑂‘𝑋)) ∈ On) |
46 | 42, 45 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐻‘(◡𝑂‘𝑋)) ∈ On) |
47 | | oaword1 7519 |
. . . 4
⊢ ((((𝐴 ↑𝑜
𝑋)
·𝑜 (𝐺‘𝑋)) ∈ On ∧ (𝐻‘(◡𝑂‘𝑋)) ∈ On) → ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)) ⊆ (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)) +𝑜 (𝐻‘(◡𝑂‘𝑋)))) |
48 | 22, 46, 47 | syl2anc 691 |
. . 3
⊢ (𝜑 → ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)) ⊆ (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)) +𝑜 (𝐻‘(◡𝑂‘𝑋)))) |
49 | 3, 1, 2, 28, 6, 43 | cantnfsuc 8450 |
. . . . 5
⊢ ((𝜑 ∧ (◡𝑂‘𝑋) ∈ ω) → (𝐻‘suc (◡𝑂‘𝑋)) = (((𝐴 ↑𝑜 (𝑂‘(◡𝑂‘𝑋))) ·𝑜 (𝐺‘(𝑂‘(◡𝑂‘𝑋)))) +𝑜 (𝐻‘(◡𝑂‘𝑋)))) |
50 | 42, 49 | mpdan 699 |
. . . 4
⊢ (𝜑 → (𝐻‘suc (◡𝑂‘𝑋)) = (((𝐴 ↑𝑜 (𝑂‘(◡𝑂‘𝑋))) ·𝑜 (𝐺‘(𝑂‘(◡𝑂‘𝑋)))) +𝑜 (𝐻‘(◡𝑂‘𝑋)))) |
51 | | f1ocnvfv2 6433 |
. . . . . . . 8
⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) |
52 | 34, 38, 51 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) |
53 | 52 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (𝐴 ↑𝑜 (𝑂‘(◡𝑂‘𝑋))) = (𝐴 ↑𝑜 𝑋)) |
54 | 52 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (𝐺‘(𝑂‘(◡𝑂‘𝑋))) = (𝐺‘𝑋)) |
55 | 53, 54 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → ((𝐴 ↑𝑜 (𝑂‘(◡𝑂‘𝑋))) ·𝑜 (𝐺‘(𝑂‘(◡𝑂‘𝑋)))) = ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋))) |
56 | 55 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → (((𝐴 ↑𝑜 (𝑂‘(◡𝑂‘𝑋))) ·𝑜 (𝐺‘(𝑂‘(◡𝑂‘𝑋)))) +𝑜 (𝐻‘(◡𝑂‘𝑋))) = (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)) +𝑜 (𝐻‘(◡𝑂‘𝑋)))) |
57 | 50, 56 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (𝐻‘suc (◡𝑂‘𝑋)) = (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)) +𝑜 (𝐻‘(◡𝑂‘𝑋)))) |
58 | 48, 57 | sseqtr4d 3605 |
. 2
⊢ (𝜑 → ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)) ⊆ (𝐻‘suc (◡𝑂‘𝑋))) |
59 | | onss 6882 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) |
60 | 2, 59 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ⊆ On) |
61 | 60 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
62 | 12 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑋 ∈ On) |
63 | | onsseleq 5682 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) |
64 | 61, 62, 63 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) |
65 | | orcom 401 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋) ↔ (𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋)) |
66 | 64, 65 | syl6bb 275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝑋 ↔ (𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋))) |
67 | 66 | ifbid 4058 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅) = if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅)) |
68 | 67 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅))) |
69 | 68 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅)))) |
70 | 3, 1, 2 | cantnfs 8446 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) |
71 | 5, 70 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)) |
72 | 71 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐵⟶𝐴) |
73 | 72 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝐹‘𝑦) ∈ 𝐴) |
74 | | ne0i 3880 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑋) ∈ 𝐴 → 𝐴 ≠ ∅) |
75 | 18, 74 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≠ ∅) |
76 | | on0eln0 5697 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
77 | 1, 76 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
78 | 75, 77 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → ∅ ∈ 𝐴) |
79 | 78 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∅ ∈ 𝐴) |
80 | 73, 79 | ifcld 4081 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅) ∈ 𝐴) |
81 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) |
82 | 80, 81 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)):𝐵⟶𝐴) |
83 | | 0ex 4718 |
. . . . . . . . 9
⊢ ∅
∈ V |
84 | 83 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈
V) |
85 | 71 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 finSupp ∅) |
86 | 72, 2, 84, 85 | fsuppmptif 8188 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) finSupp
∅) |
87 | 3, 1, 2 | cantnfs 8446 |
. . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) ∈ 𝑆 ↔ ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)):𝐵⟶𝐴 ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) finSupp
∅))) |
88 | 82, 86, 87 | mpbir2and 959 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) ∈ 𝑆) |
89 | 72, 10 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐴) |
90 | | eldifn 3695 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐵 ∖ 𝑋) → ¬ 𝑦 ∈ 𝑋) |
91 | 90 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∖ 𝑋)) → ¬ 𝑦 ∈ 𝑋) |
92 | 91 | iffalsed 4047 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∖ 𝑋)) → if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅) = ∅) |
93 | 92, 2 | suppss2 7216 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) supp ∅) ⊆ 𝑋) |
94 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
95 | 94 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑋) → (𝐹‘𝑥) = (𝐹‘𝑋)) |
96 | 95 | ifeq1da 4066 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → if(𝑥 = 𝑋, (𝐹‘𝑥), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥)) = if(𝑥 = 𝑋, (𝐹‘𝑋), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥))) |
97 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑋 ↔ 𝑥 ∈ 𝑋)) |
98 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
99 | 97, 98 | ifbieq1d 4059 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅) = if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅)) |
100 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑥) ∈ V |
101 | 100, 83 | ifex 4106 |
. . . . . . . . . . 11
⊢ if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅) ∈ V |
102 | 99, 81, 101 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥) = if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅)) |
103 | 102 | ifeq2d 4055 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → if(𝑥 = 𝑋, (𝐹‘𝑥), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥)) = if(𝑥 = 𝑋, (𝐹‘𝑥), if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅))) |
104 | 96, 103 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → if(𝑥 = 𝑋, (𝐹‘𝑋), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥)) = if(𝑥 = 𝑋, (𝐹‘𝑥), if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅))) |
105 | | ifor 4085 |
. . . . . . . 8
⊢ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅) = if(𝑥 = 𝑋, (𝐹‘𝑥), if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅)) |
106 | 104, 105 | syl6reqr 2663 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 → if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅) = if(𝑥 = 𝑋, (𝐹‘𝑋), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥))) |
107 | 106 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 𝑋, (𝐹‘𝑋), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥))) |
108 | 3, 1, 2, 88, 10, 89, 93, 107 | cantnfp1 8461 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅))) = (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)))))) |
109 | 108 | simprd 478 |
. . . 4
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅))) = (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))))) |
110 | 69, 109 | eqtrd 2644 |
. . 3
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) = (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))))) |
111 | | onelon 5665 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ (𝐹‘𝑋) ∈ 𝐴) → (𝐹‘𝑋) ∈ On) |
112 | 1, 89, 111 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑋) ∈ On) |
113 | | omsuc 7493 |
. . . . . 6
⊢ (((𝐴 ↑𝑜
𝑋) ∈ On ∧ (𝐹‘𝑋) ∈ On) → ((𝐴 ↑𝑜 𝑋) ·𝑜
suc (𝐹‘𝑋)) = (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 (𝐴 ↑𝑜 𝑋))) |
114 | 14, 112, 113 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝐴 ↑𝑜 𝑋) ·𝑜
suc (𝐹‘𝑋)) = (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 (𝐴 ↑𝑜 𝑋))) |
115 | | eloni 5650 |
. . . . . . . 8
⊢ ((𝐺‘𝑋) ∈ On → Ord (𝐺‘𝑋)) |
116 | 20, 115 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Ord (𝐺‘𝑋)) |
117 | 9 | simp2d 1067 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝑋) ∈ (𝐺‘𝑋)) |
118 | | ordsucss 6910 |
. . . . . . 7
⊢ (Ord
(𝐺‘𝑋) → ((𝐹‘𝑋) ∈ (𝐺‘𝑋) → suc (𝐹‘𝑋) ⊆ (𝐺‘𝑋))) |
119 | 116, 117,
118 | sylc 63 |
. . . . . 6
⊢ (𝜑 → suc (𝐹‘𝑋) ⊆ (𝐺‘𝑋)) |
120 | | suceloni 6905 |
. . . . . . . 8
⊢ ((𝐹‘𝑋) ∈ On → suc (𝐹‘𝑋) ∈ On) |
121 | 112, 120 | syl 17 |
. . . . . . 7
⊢ (𝜑 → suc (𝐹‘𝑋) ∈ On) |
122 | | omwordi 7538 |
. . . . . . 7
⊢ ((suc
(𝐹‘𝑋) ∈ On ∧ (𝐺‘𝑋) ∈ On ∧ (𝐴 ↑𝑜 𝑋) ∈ On) → (suc (𝐹‘𝑋) ⊆ (𝐺‘𝑋) → ((𝐴 ↑𝑜 𝑋) ·𝑜
suc (𝐹‘𝑋)) ⊆ ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)))) |
123 | 121, 20, 14, 122 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (suc (𝐹‘𝑋) ⊆ (𝐺‘𝑋) → ((𝐴 ↑𝑜 𝑋) ·𝑜
suc (𝐹‘𝑋)) ⊆ ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋)))) |
124 | 119, 123 | mpd 15 |
. . . . 5
⊢ (𝜑 → ((𝐴 ↑𝑜 𝑋) ·𝑜
suc (𝐹‘𝑋)) ⊆ ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋))) |
125 | 114, 124 | eqsstr3d 3603 |
. . . 4
⊢ (𝜑 → (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 (𝐴 ↑𝑜 𝑋)) ⊆ ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋))) |
126 | 3, 1, 2, 88, 78, 12, 93 | cantnflt2 8453 |
. . . . 5
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ (𝐴 ↑𝑜 𝑋)) |
127 | | onelon 5665 |
. . . . . . 7
⊢ (((𝐴 ↑𝑜
𝑋) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ (𝐴 ↑𝑜 𝑋)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ On) |
128 | 14, 126, 127 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ On) |
129 | | omcl 7503 |
. . . . . . 7
⊢ (((𝐴 ↑𝑜
𝑋) ∈ On ∧ (𝐹‘𝑋) ∈ On) → ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) ∈ On) |
130 | 14, 112, 129 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) ∈ On) |
131 | | oaord 7514 |
. . . . . 6
⊢ ((((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ On ∧ (𝐴 ↑𝑜
𝑋) ∈ On ∧ ((𝐴 ↑𝑜
𝑋)
·𝑜 (𝐹‘𝑋)) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ (𝐴 ↑𝑜 𝑋) ↔ (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)))) ∈ (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 (𝐴 ↑𝑜 𝑋)))) |
132 | 128, 14, 130, 131 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ (𝐴 ↑𝑜 𝑋) ↔ (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)))) ∈ (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 (𝐴 ↑𝑜 𝑋)))) |
133 | 126, 132 | mpbid 221 |
. . . 4
⊢ (𝜑 → (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)))) ∈ (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 (𝐴 ↑𝑜 𝑋))) |
134 | 125, 133 | sseldd 3569 |
. . 3
⊢ (𝜑 → (((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐹‘𝑋)) +𝑜 ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)))) ∈ ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋))) |
135 | 110, 134 | eqeltrd 2688 |
. 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ ((𝐴 ↑𝑜 𝑋) ·𝑜
(𝐺‘𝑋))) |
136 | 58, 135 | sseldd 3569 |
1
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋))) |