| Step | Hyp | Ref
| Expression |
| 1 | | cantnfs.s |
. . 3
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
| 2 | | cantnfs.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ On) |
| 3 | | cantnfs.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ On) |
| 4 | | eqid 2737 |
. . 3
⊢ OrdIso( E
, ((𝐵 × {∅})
supp ∅)) = OrdIso( E , ((𝐵 × {∅}) supp
∅)) |
| 5 | | cantnf0.a |
. . . . 5
⊢ (𝜑 → ∅ ∈ 𝐴) |
| 6 | | fconst6g 6797 |
. . . . 5
⊢ (∅
∈ 𝐴 → (𝐵 × {∅}):𝐵⟶𝐴) |
| 7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐵 × {∅}):𝐵⟶𝐴) |
| 8 | 3, 5 | fczfsuppd 9426 |
. . . 4
⊢ (𝜑 → (𝐵 × {∅}) finSupp
∅) |
| 9 | 1, 2, 3 | cantnfs 9706 |
. . . 4
⊢ (𝜑 → ((𝐵 × {∅}) ∈ 𝑆 ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp
∅))) |
| 10 | 7, 8, 9 | mpbir2and 713 |
. . 3
⊢ (𝜑 → (𝐵 × {∅}) ∈ 𝑆) |
| 11 | | eqid 2737 |
. . 3
⊢
seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘))
·o ((𝐵
× {∅})‘(OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘)))
+o 𝑧)), ∅)
= seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘))
·o ((𝐵
× {∅})‘(OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘)))
+o 𝑧)),
∅) |
| 12 | 1, 2, 3, 4, 10, 11 | cantnfval 9708 |
. 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) =
(seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘))
·o ((𝐵
× {∅})‘(OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘)))
+o 𝑧)),
∅)‘dom OrdIso( E , ((𝐵 × {∅}) supp
∅)))) |
| 13 | | eqidd 2738 |
. . . . . . 7
⊢ (𝜑 → (𝐵 × {∅}) = (𝐵 × {∅})) |
| 14 | | 0ex 5307 |
. . . . . . . . 9
⊢ ∅
∈ V |
| 15 | | fnconstg 6796 |
. . . . . . . . 9
⊢ (∅
∈ V → (𝐵 ×
{∅}) Fn 𝐵) |
| 16 | 14, 15 | mp1i 13 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 × {∅}) Fn 𝐵) |
| 17 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈
V) |
| 18 | | fnsuppeq0 8217 |
. . . . . . . 8
⊢ (((𝐵 × {∅}) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(((𝐵 × {∅})
supp ∅) = ∅ ↔ (𝐵 × {∅}) = (𝐵 × {∅}))) |
| 19 | 16, 3, 17, 18 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (((𝐵 × {∅}) supp ∅) = ∅
↔ (𝐵 ×
{∅}) = (𝐵 ×
{∅}))) |
| 20 | 13, 19 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → ((𝐵 × {∅}) supp ∅) =
∅) |
| 21 | | oieq2 9553 |
. . . . . 6
⊢ (((𝐵 × {∅}) supp
∅) = ∅ → OrdIso( E , ((𝐵 × {∅}) supp ∅)) = OrdIso(
E , ∅)) |
| 22 | 20, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → OrdIso( E , ((𝐵 × {∅}) supp
∅)) = OrdIso( E , ∅)) |
| 23 | 22 | dmeqd 5916 |
. . . 4
⊢ (𝜑 → dom OrdIso( E , ((𝐵 × {∅}) supp
∅)) = dom OrdIso( E , ∅)) |
| 24 | | we0 5680 |
. . . . . 6
⊢ E We
∅ |
| 25 | | eqid 2737 |
. . . . . . 7
⊢ OrdIso( E
, ∅) = OrdIso( E , ∅) |
| 26 | 25 | oien 9578 |
. . . . . 6
⊢ ((∅
∈ V ∧ E We ∅) → dom OrdIso( E , ∅) ≈
∅) |
| 27 | 14, 24, 26 | mp2an 692 |
. . . . 5
⊢ dom
OrdIso( E , ∅) ≈ ∅ |
| 28 | | en0 9058 |
. . . . 5
⊢ (dom
OrdIso( E , ∅) ≈ ∅ ↔ dom OrdIso( E , ∅) =
∅) |
| 29 | 27, 28 | mpbi 230 |
. . . 4
⊢ dom
OrdIso( E , ∅) = ∅ |
| 30 | 23, 29 | eqtrdi 2793 |
. . 3
⊢ (𝜑 → dom OrdIso( E , ((𝐵 × {∅}) supp
∅)) = ∅) |
| 31 | 30 | fveq2d 6910 |
. 2
⊢ (𝜑 →
(seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘))
·o ((𝐵
× {∅})‘(OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘)))
+o 𝑧)),
∅)‘dom OrdIso( E , ((𝐵 × {∅}) supp ∅))) =
(seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘))
·o ((𝐵
× {∅})‘(OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘)))
+o 𝑧)),
∅)‘∅)) |
| 32 | 11 | seqom0g 8496 |
. . 3
⊢ (∅
∈ V → (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘))
·o ((𝐵
× {∅})‘(OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘)))
+o 𝑧)),
∅)‘∅) = ∅) |
| 33 | 14, 32 | mp1i 13 |
. 2
⊢ (𝜑 →
(seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘))
·o ((𝐵
× {∅})‘(OrdIso( E , ((𝐵 × {∅}) supp
∅))‘𝑘)))
+o 𝑧)),
∅)‘∅) = ∅) |
| 34 | 12, 31, 33 | 3eqtrd 2781 |
1
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) =
∅) |