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 9725 | . . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) | 
| 10 | 9 | simp1d 1142 | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 11 |  | onelon 6408 | . . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On) | 
| 12 | 2, 10, 11 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ On) | 
| 13 |  | oecl 8576 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴 ↑o 𝑋) ∈ On) | 
| 14 | 1, 12, 13 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐴 ↑o 𝑋) ∈ On) | 
| 15 | 3, 1, 2 | cantnfs 9707 | . . . . . . . . 9
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) | 
| 16 | 6, 15 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) | 
| 17 | 16 | simpld 494 | . . . . . . 7
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) | 
| 18 | 17, 10 | ffvelcdmd 7104 | . . . . . 6
⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴) | 
| 19 |  | onelon 6408 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ (𝐺‘𝑋) ∈ 𝐴) → (𝐺‘𝑋) ∈ On) | 
| 20 | 1, 18, 19 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐺‘𝑋) ∈ On) | 
| 21 |  | omcl 8575 | . . . . 5
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ (𝐺‘𝑋) ∈ On) → ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)) ∈ On) | 
| 22 | 14, 20, 21 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)) ∈ On) | 
| 23 |  | ovexd 7467 | . . . . . . . . . 10
⊢ (𝜑 → (𝐺 supp ∅) ∈ V) | 
| 24 |  | cantnflem1.o | . . . . . . . . . . . 12
⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅)) | 
| 25 | 3, 1, 2, 24, 6 | cantnfcl 9708 | . . . . . . . . . . 11
⊢ (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω)) | 
| 26 | 25 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → E We (𝐺 supp ∅)) | 
| 27 | 24 | oiiso 9578 | . . . . . . . . . 10
⊢ (((𝐺 supp ∅) ∈ V ∧ E
We (𝐺 supp ∅)) →
𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅))) | 
| 28 | 23, 26, 27 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅))) | 
| 29 |  | isof1o 7344 | . . . . . . . . 9
⊢ (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅)) | 
| 30 | 28, 29 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅)) | 
| 31 |  | f1ocnv 6859 | . . . . . . . 8
⊢ (𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) → ◡𝑂:(𝐺 supp ∅)–1-1-onto→dom
𝑂) | 
| 32 |  | f1of 6847 | . . . . . . . 8
⊢ (◡𝑂:(𝐺 supp ∅)–1-1-onto→dom
𝑂 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂) | 
| 33 | 30, 31, 32 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂) | 
| 34 | 3, 1, 2, 4, 5, 6, 7, 8 | cantnflem1a 9726 | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅)) | 
| 35 | 33, 34 | ffvelcdmd 7104 | . . . . . 6
⊢ (𝜑 → (◡𝑂‘𝑋) ∈ dom 𝑂) | 
| 36 | 25 | simprd 495 | . . . . . 6
⊢ (𝜑 → dom 𝑂 ∈ ω) | 
| 37 |  | elnn 7899 | . . . . . 6
⊢ (((◡𝑂‘𝑋) ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (◡𝑂‘𝑋) ∈ ω) | 
| 38 | 35, 36, 37 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (◡𝑂‘𝑋) ∈ ω) | 
| 39 |  | cantnflem1.h | . . . . . . 7
⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝑂‘𝑘)) ·o (𝐺‘(𝑂‘𝑘))) +o 𝑧)), ∅) | 
| 40 | 39 | cantnfvalf 9706 | . . . . . 6
⊢ 𝐻:ω⟶On | 
| 41 | 40 | ffvelcdmi 7102 | . . . . 5
⊢ ((◡𝑂‘𝑋) ∈ ω → (𝐻‘(◡𝑂‘𝑋)) ∈ On) | 
| 42 | 38, 41 | syl 17 | . . . 4
⊢ (𝜑 → (𝐻‘(◡𝑂‘𝑋)) ∈ On) | 
| 43 |  | oaword1 8591 | . . . 4
⊢ ((((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)) ∈ On ∧ (𝐻‘(◡𝑂‘𝑋)) ∈ On) → ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)) ⊆ (((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)) +o (𝐻‘(◡𝑂‘𝑋)))) | 
| 44 | 22, 42, 43 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)) ⊆ (((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)) +o (𝐻‘(◡𝑂‘𝑋)))) | 
| 45 | 3, 1, 2, 24, 6, 39 | cantnfsuc 9711 | . . . . 5
⊢ ((𝜑 ∧ (◡𝑂‘𝑋) ∈ ω) → (𝐻‘suc (◡𝑂‘𝑋)) = (((𝐴 ↑o (𝑂‘(◡𝑂‘𝑋))) ·o (𝐺‘(𝑂‘(◡𝑂‘𝑋)))) +o (𝐻‘(◡𝑂‘𝑋)))) | 
| 46 | 38, 45 | mpdan 687 | . . . 4
⊢ (𝜑 → (𝐻‘suc (◡𝑂‘𝑋)) = (((𝐴 ↑o (𝑂‘(◡𝑂‘𝑋))) ·o (𝐺‘(𝑂‘(◡𝑂‘𝑋)))) +o (𝐻‘(◡𝑂‘𝑋)))) | 
| 47 |  | f1ocnvfv2 7298 | . . . . . . . 8
⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) | 
| 48 | 30, 34, 47 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) | 
| 49 | 48 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (𝐴 ↑o (𝑂‘(◡𝑂‘𝑋))) = (𝐴 ↑o 𝑋)) | 
| 50 | 48 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 → (𝐺‘(𝑂‘(◡𝑂‘𝑋))) = (𝐺‘𝑋)) | 
| 51 | 49, 50 | oveq12d 7450 | . . . . 5
⊢ (𝜑 → ((𝐴 ↑o (𝑂‘(◡𝑂‘𝑋))) ·o (𝐺‘(𝑂‘(◡𝑂‘𝑋)))) = ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋))) | 
| 52 | 51 | oveq1d 7447 | . . . 4
⊢ (𝜑 → (((𝐴 ↑o (𝑂‘(◡𝑂‘𝑋))) ·o (𝐺‘(𝑂‘(◡𝑂‘𝑋)))) +o (𝐻‘(◡𝑂‘𝑋))) = (((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)) +o (𝐻‘(◡𝑂‘𝑋)))) | 
| 53 | 46, 52 | eqtrd 2776 | . . 3
⊢ (𝜑 → (𝐻‘suc (◡𝑂‘𝑋)) = (((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)) +o (𝐻‘(◡𝑂‘𝑋)))) | 
| 54 | 44, 53 | sseqtrrd 4020 | . 2
⊢ (𝜑 → ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)) ⊆ (𝐻‘suc (◡𝑂‘𝑋))) | 
| 55 |  | onss 7806 | . . . . . . . . . . 11
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) | 
| 56 | 2, 55 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ⊆ On) | 
| 57 | 56 | sselda 3982 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) | 
| 58 | 12 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑋 ∈ On) | 
| 59 |  | onsseleq 6424 | . . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) | 
| 60 | 57, 58, 59 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝑋 ↔ (𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋))) | 
| 61 |  | orcom 870 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋) ↔ (𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋)) | 
| 62 | 60, 61 | bitrdi 287 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝑋 ↔ (𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋))) | 
| 63 | 62 | ifbid 4548 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅) = if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅)) | 
| 64 | 63 | mpteq2dva 5241 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅))) | 
| 65 | 64 | fveq2d 6909 | . . . 4
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅)))) | 
| 66 | 3, 1, 2 | cantnfs 9707 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) | 
| 67 | 5, 66 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)) | 
| 68 | 67 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐵⟶𝐴) | 
| 69 | 68 | ffvelcdmda 7103 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝐹‘𝑦) ∈ 𝐴) | 
| 70 | 18 | ne0d 4341 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≠ ∅) | 
| 71 |  | on0eln0 6439 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) | 
| 72 | 1, 71 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) | 
| 73 | 70, 72 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → ∅ ∈ 𝐴) | 
| 74 | 73 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∅ ∈ 𝐴) | 
| 75 | 69, 74 | ifcld 4571 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅) ∈ 𝐴) | 
| 76 | 75 | fmpttd 7134 | . . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)):𝐵⟶𝐴) | 
| 77 |  | 0ex 5306 | . . . . . . . . 9
⊢ ∅
∈ V | 
| 78 | 77 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → ∅ ∈
V) | 
| 79 | 67 | simprd 495 | . . . . . . . 8
⊢ (𝜑 → 𝐹 finSupp ∅) | 
| 80 | 68, 2, 78, 79 | fsuppmptif 9440 | . . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) finSupp
∅) | 
| 81 | 3, 1, 2 | cantnfs 9707 | . . . . . . 7
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) ∈ 𝑆 ↔ ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)):𝐵⟶𝐴 ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) finSupp
∅))) | 
| 82 | 76, 80, 81 | mpbir2and 713 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) ∈ 𝑆) | 
| 83 | 68, 10 | ffvelcdmd 7104 | . . . . . 6
⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐴) | 
| 84 |  | eldifn 4131 | . . . . . . . . 9
⊢ (𝑦 ∈ (𝐵 ∖ 𝑋) → ¬ 𝑦 ∈ 𝑋) | 
| 85 | 84 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∖ 𝑋)) → ¬ 𝑦 ∈ 𝑋) | 
| 86 | 85 | iffalsed 4535 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∖ 𝑋)) → if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅) = ∅) | 
| 87 | 86, 2 | suppss2 8226 | . . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) supp ∅) ⊆ 𝑋) | 
| 88 |  | ifor 4579 | . . . . . . . 8
⊢ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅) = if(𝑥 = 𝑋, (𝐹‘𝑥), if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅)) | 
| 89 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) | 
| 90 | 89 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑋) → (𝐹‘𝑥) = (𝐹‘𝑋)) | 
| 91 | 90 | ifeq1da 4556 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → if(𝑥 = 𝑋, (𝐹‘𝑥), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥)) = if(𝑥 = 𝑋, (𝐹‘𝑋), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥))) | 
| 92 |  | eleq1w 2823 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑋 ↔ 𝑥 ∈ 𝑋)) | 
| 93 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) | 
| 94 | 92, 93 | ifbieq1d 4549 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅) = if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅)) | 
| 95 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)) | 
| 96 |  | fvex 6918 | . . . . . . . . . . . 12
⊢ (𝐹‘𝑥) ∈ V | 
| 97 | 96, 77 | ifex 4575 | . . . . . . . . . . 11
⊢ if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅) ∈ V | 
| 98 | 94, 95, 97 | fvmpt 7015 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥) = if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅)) | 
| 99 | 98 | ifeq2d 4545 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → if(𝑥 = 𝑋, (𝐹‘𝑥), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥)) = if(𝑥 = 𝑋, (𝐹‘𝑥), if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅))) | 
| 100 | 91, 99 | eqtr3d 2778 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → if(𝑥 = 𝑋, (𝐹‘𝑋), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥)) = if(𝑥 = 𝑋, (𝐹‘𝑥), if(𝑥 ∈ 𝑋, (𝐹‘𝑥), ∅))) | 
| 101 | 88, 100 | eqtr4id 2795 | . . . . . . 7
⊢ (𝑥 ∈ 𝐵 → if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅) = if(𝑥 = 𝑋, (𝐹‘𝑋), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥))) | 
| 102 | 101 | mpteq2ia 5244 | . . . . . 6
⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 𝑋, (𝐹‘𝑋), ((𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))‘𝑥))) | 
| 103 | 3, 1, 2, 82, 10, 83, 87, 102 | cantnfp1 9722 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅))) = (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)))))) | 
| 104 | 103 | simprd 495 | . . . 4
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋), (𝐹‘𝑥), ∅))) = (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))))) | 
| 105 | 65, 104 | eqtrd 2776 | . . 3
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) = (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))))) | 
| 106 |  | onelon 6408 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ (𝐹‘𝑋) ∈ 𝐴) → (𝐹‘𝑋) ∈ On) | 
| 107 | 1, 83, 106 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝐹‘𝑋) ∈ On) | 
| 108 |  | omsuc 8565 | . . . . . 6
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ (𝐹‘𝑋) ∈ On) → ((𝐴 ↑o 𝑋) ·o suc (𝐹‘𝑋)) = (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o (𝐴 ↑o 𝑋))) | 
| 109 | 14, 107, 108 | syl2anc 584 | . . . . 5
⊢ (𝜑 → ((𝐴 ↑o 𝑋) ·o suc (𝐹‘𝑋)) = (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o (𝐴 ↑o 𝑋))) | 
| 110 |  | eloni 6393 | . . . . . . . 8
⊢ ((𝐺‘𝑋) ∈ On → Ord (𝐺‘𝑋)) | 
| 111 | 20, 110 | syl 17 | . . . . . . 7
⊢ (𝜑 → Ord (𝐺‘𝑋)) | 
| 112 | 9 | simp2d 1143 | . . . . . . 7
⊢ (𝜑 → (𝐹‘𝑋) ∈ (𝐺‘𝑋)) | 
| 113 |  | ordsucss 7839 | . . . . . . 7
⊢ (Ord
(𝐺‘𝑋) → ((𝐹‘𝑋) ∈ (𝐺‘𝑋) → suc (𝐹‘𝑋) ⊆ (𝐺‘𝑋))) | 
| 114 | 111, 112,
113 | sylc 65 | . . . . . 6
⊢ (𝜑 → suc (𝐹‘𝑋) ⊆ (𝐺‘𝑋)) | 
| 115 |  | onsuc 7832 | . . . . . . . 8
⊢ ((𝐹‘𝑋) ∈ On → suc (𝐹‘𝑋) ∈ On) | 
| 116 | 107, 115 | syl 17 | . . . . . . 7
⊢ (𝜑 → suc (𝐹‘𝑋) ∈ On) | 
| 117 |  | omwordi 8610 | . . . . . . 7
⊢ ((suc
(𝐹‘𝑋) ∈ On ∧ (𝐺‘𝑋) ∈ On ∧ (𝐴 ↑o 𝑋) ∈ On) → (suc (𝐹‘𝑋) ⊆ (𝐺‘𝑋) → ((𝐴 ↑o 𝑋) ·o suc (𝐹‘𝑋)) ⊆ ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)))) | 
| 118 | 116, 20, 14, 117 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (suc (𝐹‘𝑋) ⊆ (𝐺‘𝑋) → ((𝐴 ↑o 𝑋) ·o suc (𝐹‘𝑋)) ⊆ ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋)))) | 
| 119 | 114, 118 | mpd 15 | . . . . 5
⊢ (𝜑 → ((𝐴 ↑o 𝑋) ·o suc (𝐹‘𝑋)) ⊆ ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋))) | 
| 120 | 109, 119 | eqsstrrd 4018 | . . . 4
⊢ (𝜑 → (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o (𝐴 ↑o 𝑋)) ⊆ ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋))) | 
| 121 | 3, 1, 2, 82, 73, 12, 87 | cantnflt2 9714 | . . . . 5
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ (𝐴 ↑o 𝑋)) | 
| 122 |  | onelon 6408 | . . . . . . 7
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ (𝐴 ↑o 𝑋)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ On) | 
| 123 | 14, 121, 122 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ On) | 
| 124 |  | omcl 8575 | . . . . . . 7
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ (𝐹‘𝑋) ∈ On) → ((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) ∈ On) | 
| 125 | 14, 107, 124 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) ∈ On) | 
| 126 |  | oaord 8586 | . . . . . 6
⊢ ((((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ On ∧ (𝐴 ↑o 𝑋) ∈ On ∧ ((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ (𝐴 ↑o 𝑋) ↔ (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)))) ∈ (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o (𝐴 ↑o 𝑋)))) | 
| 127 | 123, 14, 125, 126 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅))) ∈ (𝐴 ↑o 𝑋) ↔ (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)))) ∈ (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o (𝐴 ↑o 𝑋)))) | 
| 128 | 121, 127 | mpbid 232 | . . . 4
⊢ (𝜑 → (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)))) ∈ (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o (𝐴 ↑o 𝑋))) | 
| 129 | 120, 128 | sseldd 3983 | . . 3
⊢ (𝜑 → (((𝐴 ↑o 𝑋) ·o (𝐹‘𝑋)) +o ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 ∈ 𝑋, (𝐹‘𝑦), ∅)))) ∈ ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋))) | 
| 130 | 105, 129 | eqeltrd 2840 | . 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ ((𝐴 ↑o 𝑋) ·o (𝐺‘𝑋))) | 
| 131 | 54, 130 | sseldd 3983 | 1
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋))) |