Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. 2
⊢ dom
(ω CNF 𝐴) = dom
(ω CNF 𝐴) |
2 | | eqid 2610 |
. 2
⊢ (◡(ω CNF 𝐴)‘𝑏) = (◡(ω CNF 𝐴)‘𝑏) |
3 | | eqid 2610 |
. 2
⊢ OrdIso( E
, ((◡(ω CNF 𝐴)‘𝑏) supp ∅)) = OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)) |
4 | | eqid 2610 |
. 2
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) |
5 | | eqid 2610 |
. 2
⊢
seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ ((𝑥 ∈ ((ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) +𝑜 𝑥)))), ∅) =
seq𝜔((𝑘
∈ V, 𝑓 ∈ V
↦ ((𝑥 ∈
((ω ↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) +𝑜 𝑥)))), ∅) |
6 | | eqid 2610 |
. 2
⊢ ((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) = ((ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) |
7 | | eqid 2610 |
. 2
⊢ ((𝑥 ∈ ((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) +𝑜 𝑥))) = ((𝑥 ∈ ((ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) +𝑜 𝑥))) |
8 | | eqid 2610 |
. 2
⊢ (OrdIso(
E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))) = (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))) |
9 | | eqid 2610 |
. 2
⊢ (𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ ((((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑣) +𝑜 𝑢)) = (𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ ((((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑣) +𝑜 𝑢)) |
10 | | eqid 2610 |
. 2
⊢ (𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑢) +𝑜 𝑣)) = (𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑢) +𝑜 𝑣)) |
11 | | eqid 2610 |
. 2
⊢ (((𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ ((((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑣) +𝑜 𝑢)) ∘ ◡(𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑢) +𝑜 𝑣))) ∘ (seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ ((𝑥 ∈ ((ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) +𝑜 𝑥)))), ∅)‘dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) = (((𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ ((((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑣) +𝑜 𝑢)) ∘ ◡(𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑢) +𝑜 𝑣))) ∘ (seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ ((𝑥 ∈ ((ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) +𝑜 𝑥)))), ∅)‘dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) |
12 | | eqid 2610 |
. 2
⊢ (𝑏 ∈ (ω
↑𝑜 𝐴) ↦ (((𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ ((((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑣) +𝑜 𝑢)) ∘ ◡(𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑢) +𝑜 𝑣))) ∘ (seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ ((𝑥 ∈ ((ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) +𝑜 𝑥)))), ∅)‘dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))) = (𝑏 ∈ (ω ↑𝑜
𝐴) ↦ (((𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ ((((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑣) +𝑜 𝑢)) ∘ ◡(𝑢 ∈ ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))), 𝑣 ∈ (ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅)))) ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘∪ dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))
·𝑜 𝑢) +𝑜 𝑣))) ∘ (seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ ((𝑥 ∈ ((ω ↑𝑜
(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) ↦ (dom 𝑓 +𝑜 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (((ω
↑𝑜 (OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘)) ·𝑜 ((◡(ω CNF 𝐴)‘𝑏)‘(OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))‘𝑘))) +𝑜 𝑥)))), ∅)‘dom OrdIso( E , ((◡(ω CNF 𝐴)‘𝑏) supp ∅))))) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | cnfcom3clem 8485 |
1
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |