| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cantnfs.s | . . . . 5
⊢ 𝑆 = dom (𝐴 CNF 𝐵) | 
| 2 |  | cantnfs.a | . . . . 5
⊢ (𝜑 → 𝐴 ∈ On) | 
| 3 |  | cantnfs.b | . . . . 5
⊢ (𝜑 → 𝐵 ∈ On) | 
| 4 |  | cantnf.g | . . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝑆) | 
| 5 |  | oemapval.t | . . . . . . . . . . . . . 14
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} | 
| 6 |  | cantnf.c | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑o 𝐵)) | 
| 7 |  | cantnf.s | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵)) | 
| 8 |  | cantnf.e | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∅ ∈ 𝐶) | 
| 9 | 1, 2, 3, 5, 6, 7, 8 | cantnflem2 9731 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ (On ∖ 2o) ∧
𝐶 ∈ (On ∖
1o))) | 
| 10 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ 𝑋 = 𝑋 | 
| 11 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ 𝑌 = 𝑌 | 
| 12 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ 𝑍 = 𝑍 | 
| 13 | 10, 11, 12 | 3pm3.2i 1339 | . . . . . . . . . . . . . 14
⊢ (𝑋 = 𝑋 ∧ 𝑌 = 𝑌 ∧ 𝑍 = 𝑍) | 
| 14 |  | cantnf.x | . . . . . . . . . . . . . . 15
⊢ 𝑋 = ∪
∩ {𝑐 ∈ On ∣ 𝐶 ∈ (𝐴 ↑o 𝑐)} | 
| 15 |  | cantnf.p | . . . . . . . . . . . . . . 15
⊢ 𝑃 = (℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑o 𝑋)(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑o 𝑋) ·o 𝑎) +o 𝑏) = 𝐶)) | 
| 16 |  | cantnf.y | . . . . . . . . . . . . . . 15
⊢ 𝑌 = (1st ‘𝑃) | 
| 17 |  | cantnf.z | . . . . . . . . . . . . . . 15
⊢ 𝑍 = (2nd ‘𝑃) | 
| 18 | 14, 15, 16, 17 | oeeui 8641 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐶
∈ (On ∖ 1o)) → (((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴 ↑o 𝑋)) ∧ (((𝐴 ↑o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶) ↔ (𝑋 = 𝑋 ∧ 𝑌 = 𝑌 ∧ 𝑍 = 𝑍))) | 
| 19 | 13, 18 | mpbiri 258 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐶
∈ (On ∖ 1o)) → ((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴 ↑o 𝑋)) ∧ (((𝐴 ↑o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶)) | 
| 20 | 9, 19 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴 ↑o 𝑋)) ∧ (((𝐴 ↑o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶)) | 
| 21 | 20 | simpld 494 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1o) ∧ 𝑍 ∈ (𝐴 ↑o 𝑋))) | 
| 22 | 21 | simp1d 1142 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ On) | 
| 23 |  | oecl 8576 | . . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴 ↑o 𝑋) ∈ On) | 
| 24 | 2, 22, 23 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 ↑o 𝑋) ∈ On) | 
| 25 | 21 | simp2d 1143 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ (𝐴 ∖ 1o)) | 
| 26 | 25 | eldifad 3962 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝐴) | 
| 27 |  | onelon 6408 | . . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑌 ∈ 𝐴) → 𝑌 ∈ On) | 
| 28 | 2, 26, 27 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ On) | 
| 29 |  | dif1o 8539 | . . . . . . . . . . . 12
⊢ (𝑌 ∈ (𝐴 ∖ 1o) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌 ≠ ∅)) | 
| 30 | 29 | simprbi 496 | . . . . . . . . . . 11
⊢ (𝑌 ∈ (𝐴 ∖ 1o) → 𝑌 ≠ ∅) | 
| 31 | 25, 30 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ≠ ∅) | 
| 32 |  | on0eln0 6439 | . . . . . . . . . . 11
⊢ (𝑌 ∈ On → (∅
∈ 𝑌 ↔ 𝑌 ≠ ∅)) | 
| 33 | 28, 32 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅)) | 
| 34 | 31, 33 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → ∅ ∈ 𝑌) | 
| 35 |  | omword1 8612 | . . . . . . . . 9
⊢ ((((𝐴 ↑o 𝑋) ∈ On ∧ 𝑌 ∈ On) ∧ ∅ ∈
𝑌) → (𝐴 ↑o 𝑋) ⊆ ((𝐴 ↑o 𝑋) ·o 𝑌)) | 
| 36 | 24, 28, 34, 35 | syl21anc 837 | . . . . . . . 8
⊢ (𝜑 → (𝐴 ↑o 𝑋) ⊆ ((𝐴 ↑o 𝑋) ·o 𝑌)) | 
| 37 |  | omcl 8575 | . . . . . . . . . . 11
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ 𝑌 ∈ On) → ((𝐴 ↑o 𝑋) ·o 𝑌) ∈ On) | 
| 38 | 24, 28, 37 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ↑o 𝑋) ·o 𝑌) ∈ On) | 
| 39 | 21 | simp3d 1144 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ (𝐴 ↑o 𝑋)) | 
| 40 |  | onelon 6408 | . . . . . . . . . . 11
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ 𝑍 ∈ (𝐴 ↑o 𝑋)) → 𝑍 ∈ On) | 
| 41 | 24, 39, 40 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ On) | 
| 42 |  | oaword1 8591 | . . . . . . . . . 10
⊢ ((((𝐴 ↑o 𝑋) ·o 𝑌) ∈ On ∧ 𝑍 ∈ On) → ((𝐴 ↑o 𝑋) ·o 𝑌) ⊆ (((𝐴 ↑o 𝑋) ·o 𝑌) +o 𝑍)) | 
| 43 | 38, 41, 42 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → ((𝐴 ↑o 𝑋) ·o 𝑌) ⊆ (((𝐴 ↑o 𝑋) ·o 𝑌) +o 𝑍)) | 
| 44 | 20 | simprd 495 | . . . . . . . . 9
⊢ (𝜑 → (((𝐴 ↑o 𝑋) ·o 𝑌) +o 𝑍) = 𝐶) | 
| 45 | 43, 44 | sseqtrd 4019 | . . . . . . . 8
⊢ (𝜑 → ((𝐴 ↑o 𝑋) ·o 𝑌) ⊆ 𝐶) | 
| 46 | 36, 45 | sstrd 3993 | . . . . . . 7
⊢ (𝜑 → (𝐴 ↑o 𝑋) ⊆ 𝐶) | 
| 47 |  | oecl 8576 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) ∈ On) | 
| 48 | 2, 3, 47 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐴 ↑o 𝐵) ∈ On) | 
| 49 |  | ontr2 6430 | . . . . . . . 8
⊢ (((𝐴 ↑o 𝑋) ∈ On ∧ (𝐴 ↑o 𝐵) ∈ On) → (((𝐴 ↑o 𝑋) ⊆ 𝐶 ∧ 𝐶 ∈ (𝐴 ↑o 𝐵)) → (𝐴 ↑o 𝑋) ∈ (𝐴 ↑o 𝐵))) | 
| 50 | 24, 48, 49 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (((𝐴 ↑o 𝑋) ⊆ 𝐶 ∧ 𝐶 ∈ (𝐴 ↑o 𝐵)) → (𝐴 ↑o 𝑋) ∈ (𝐴 ↑o 𝐵))) | 
| 51 | 46, 6, 50 | mp2and 699 | . . . . . 6
⊢ (𝜑 → (𝐴 ↑o 𝑋) ∈ (𝐴 ↑o 𝐵)) | 
| 52 | 9 | simpld 494 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (On ∖
2o)) | 
| 53 |  | oeord 8627 | . . . . . . 7
⊢ ((𝑋 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ (On ∖
2o)) → (𝑋
∈ 𝐵 ↔ (𝐴 ↑o 𝑋) ∈ (𝐴 ↑o 𝐵))) | 
| 54 | 22, 3, 52, 53 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ (𝐴 ↑o 𝑋) ∈ (𝐴 ↑o 𝐵))) | 
| 55 | 51, 54 | mpbird 257 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 56 | 2 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝐴 ∈ On) | 
| 57 | 3 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝐵 ∈ On) | 
| 58 |  | suppssdm 8203 | . . . . . . . . . . . . . . 15
⊢ (𝐺 supp ∅) ⊆ dom 𝐺 | 
| 59 | 1, 2, 3 | cantnfs 9707 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) | 
| 60 | 4, 59 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) | 
| 61 | 60 | simpld 494 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) | 
| 62 | 58, 61 | fssdm 6754 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵) | 
| 63 | 62 | sselda 3982 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑥 ∈ 𝐵) | 
| 64 |  | onelon 6408 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) | 
| 65 | 57, 63, 64 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑥 ∈ On) | 
| 66 |  | oecl 8576 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ↑o 𝑥) ∈ On) | 
| 67 | 56, 65, 66 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐴 ↑o 𝑥) ∈ On) | 
| 68 | 61 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝐺:𝐵⟶𝐴) | 
| 69 | 68, 63 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐺‘𝑥) ∈ 𝐴) | 
| 70 |  | onelon 6408 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (𝐺‘𝑥) ∈ 𝐴) → (𝐺‘𝑥) ∈ On) | 
| 71 | 56, 69, 70 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐺‘𝑥) ∈ On) | 
| 72 | 61 | ffnd 6736 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 Fn 𝐵) | 
| 73 | 8 | elexd 3503 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∅ ∈
V) | 
| 74 |  | elsuppfn 8196 | . . . . . . . . . . . . . 14
⊢ ((𝐺 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(𝑥 ∈ (𝐺 supp ∅) ↔ (𝑥 ∈ 𝐵 ∧ (𝐺‘𝑥) ≠ ∅))) | 
| 75 | 72, 3, 73, 74 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝐺 supp ∅) ↔ (𝑥 ∈ 𝐵 ∧ (𝐺‘𝑥) ≠ ∅))) | 
| 76 | 75 | simplbda 499 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐺‘𝑥) ≠ ∅) | 
| 77 |  | on0eln0 6439 | . . . . . . . . . . . . 13
⊢ ((𝐺‘𝑥) ∈ On → (∅ ∈ (𝐺‘𝑥) ↔ (𝐺‘𝑥) ≠ ∅)) | 
| 78 | 71, 77 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∅ ∈
(𝐺‘𝑥) ↔ (𝐺‘𝑥) ≠ ∅)) | 
| 79 | 76, 78 | mpbird 257 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∅ ∈ (𝐺‘𝑥)) | 
| 80 |  | omword1 8612 | . . . . . . . . . . 11
⊢ ((((𝐴 ↑o 𝑥) ∈ On ∧ (𝐺‘𝑥) ∈ On) ∧ ∅ ∈ (𝐺‘𝑥)) → (𝐴 ↑o 𝑥) ⊆ ((𝐴 ↑o 𝑥) ·o (𝐺‘𝑥))) | 
| 81 | 67, 71, 79, 80 | syl21anc 837 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐴 ↑o 𝑥) ⊆ ((𝐴 ↑o 𝑥) ·o (𝐺‘𝑥))) | 
| 82 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ OrdIso( E
, (𝐺 supp ∅)) =
OrdIso( E , (𝐺 supp
∅)) | 
| 83 | 4 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝐺 ∈ 𝑆) | 
| 84 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (OrdIso( E , (𝐺 supp ∅))‘𝑘)) ·o (𝐺‘(OrdIso( E , (𝐺 supp ∅))‘𝑘))) +o 𝑧)), ∅) =
seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , (𝐺 supp ∅))‘𝑘)) ·o (𝐺‘(OrdIso( E , (𝐺 supp ∅))‘𝑘))) +o 𝑧)), ∅) | 
| 85 | 1, 56, 57, 82, 83, 84, 63 | cantnfle 9712 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝐴 ↑o 𝑥) ·o (𝐺‘𝑥)) ⊆ ((𝐴 CNF 𝐵)‘𝐺)) | 
| 86 |  | cantnf.v | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍) | 
| 87 | 86 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍) | 
| 88 | 85, 87 | sseqtrd 4019 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝐴 ↑o 𝑥) ·o (𝐺‘𝑥)) ⊆ 𝑍) | 
| 89 | 81, 88 | sstrd 3993 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐴 ↑o 𝑥) ⊆ 𝑍) | 
| 90 | 39 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑍 ∈ (𝐴 ↑o 𝑋)) | 
| 91 | 24 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐴 ↑o 𝑋) ∈ On) | 
| 92 |  | ontr2 6430 | . . . . . . . . . 10
⊢ (((𝐴 ↑o 𝑥) ∈ On ∧ (𝐴 ↑o 𝑋) ∈ On) → (((𝐴 ↑o 𝑥) ⊆ 𝑍 ∧ 𝑍 ∈ (𝐴 ↑o 𝑋)) → (𝐴 ↑o 𝑥) ∈ (𝐴 ↑o 𝑋))) | 
| 93 | 67, 91, 92 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (((𝐴 ↑o 𝑥) ⊆ 𝑍 ∧ 𝑍 ∈ (𝐴 ↑o 𝑋)) → (𝐴 ↑o 𝑥) ∈ (𝐴 ↑o 𝑋))) | 
| 94 | 89, 90, 93 | mp2and 699 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐴 ↑o 𝑥) ∈ (𝐴 ↑o 𝑋)) | 
| 95 | 22 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑋 ∈ On) | 
| 96 | 52 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝐴 ∈ (On ∖
2o)) | 
| 97 |  | oeord 8627 | . . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖
2o)) → (𝑥
∈ 𝑋 ↔ (𝐴 ↑o 𝑥) ∈ (𝐴 ↑o 𝑋))) | 
| 98 | 65, 95, 96, 97 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑥 ∈ 𝑋 ↔ (𝐴 ↑o 𝑥) ∈ (𝐴 ↑o 𝑋))) | 
| 99 | 94, 98 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑥 ∈ 𝑋) | 
| 100 | 99 | ex 412 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐺 supp ∅) → 𝑥 ∈ 𝑋)) | 
| 101 | 100 | ssrdv 3988 | . . . . 5
⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋) | 
| 102 |  | cantnf.f | . . . . 5
⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) | 
| 103 | 1, 2, 3, 4, 55, 26, 101, 102 | cantnfp1 9722 | . . . 4
⊢ (𝜑 → (𝐹 ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))) | 
| 104 | 103 | simprd 495 | . . 3
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺))) | 
| 105 | 86 | oveq2d 7448 | . . 3
⊢ (𝜑 → (((𝐴 ↑o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)) = (((𝐴 ↑o 𝑋) ·o 𝑌) +o 𝑍)) | 
| 106 | 104, 105,
44 | 3eqtrd 2780 | . 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = 𝐶) | 
| 107 | 1, 2, 3 | cantnff 9715 | . . . 4
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑o 𝐵)) | 
| 108 | 107 | ffnd 6736 | . . 3
⊢ (𝜑 → (𝐴 CNF 𝐵) Fn 𝑆) | 
| 109 | 103 | simpld 494 | . . 3
⊢ (𝜑 → 𝐹 ∈ 𝑆) | 
| 110 |  | fnfvelrn 7099 | . . 3
⊢ (((𝐴 CNF 𝐵) Fn 𝑆 ∧ 𝐹 ∈ 𝑆) → ((𝐴 CNF 𝐵)‘𝐹) ∈ ran (𝐴 CNF 𝐵)) | 
| 111 | 108, 109,
110 | syl2anc 584 | . 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ran (𝐴 CNF 𝐵)) | 
| 112 | 106, 111 | eqeltrrd 2841 | 1
⊢ (𝜑 → 𝐶 ∈ ran (𝐴 CNF 𝐵)) |