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