| Step | Hyp | Ref
| Expression |
| 1 | | onexoegt 43256 |
. 2
⊢ (𝐴 ∈ On → ∃𝑏 ∈ On 𝐴 ∈ (ω ↑o 𝑏)) |
| 2 | | eldif 3961 |
. . . . . . 7
⊢ (𝑐 ∈ (On ∖ 𝑏) ↔ (𝑐 ∈ On ∧ ¬ 𝑐 ∈ 𝑏)) |
| 3 | | simp2 1138 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
→ 𝑏 ∈
On) |
| 4 | | pm3.2 469 |
. . . . . . . . . 10
⊢ (𝑏 ∈ On → (𝑐 ∈ On → (𝑏 ∈ On ∧ 𝑐 ∈ On))) |
| 5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
→ (𝑐 ∈ On →
(𝑏 ∈ On ∧ 𝑐 ∈ On))) |
| 6 | | ontri1 6418 |
. . . . . . . . 9
⊢ ((𝑏 ∈ On ∧ 𝑐 ∈ On) → (𝑏 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ 𝑏)) |
| 7 | 5, 6 | syl6 35 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
→ (𝑐 ∈ On →
(𝑏 ⊆ 𝑐 ↔ ¬ 𝑐 ∈ 𝑏))) |
| 8 | 7 | pm5.32d 577 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
→ ((𝑐 ∈ On ∧
𝑏 ⊆ 𝑐) ↔ (𝑐 ∈ On ∧ ¬ 𝑐 ∈ 𝑏))) |
| 9 | 2, 8 | bitr4id 290 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
→ (𝑐 ∈ (On
∖ 𝑏) ↔ (𝑐 ∈ On ∧ 𝑏 ⊆ 𝑐))) |
| 10 | | simplr 769 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑎 = 𝐴) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → 𝑎 = 𝐴) |
| 11 | 10 | breq2d 5155 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑎 = 𝐴) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → (𝑓(ω CNF 𝑐)𝑎 ↔ 𝑓(ω CNF 𝑐)𝐴)) |
| 12 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ dom
(ω CNF 𝑐) = dom
(ω CNF 𝑐) |
| 13 | | omelon 9686 |
. . . . . . . . . . . . . . 15
⊢ ω
∈ On |
| 14 | 13 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑎 = 𝐴) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → ω ∈ On) |
| 15 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → 𝑐 ∈ On) |
| 16 | 15 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑎 = 𝐴) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → 𝑐 ∈ On) |
| 17 | 12, 14, 16 | cantnff1o 9736 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑎 = 𝐴) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → (ω CNF 𝑐):dom (ω CNF 𝑐)–1-1-onto→(ω ↑o 𝑐)) |
| 18 | | f1ofun 6850 |
. . . . . . . . . . . . 13
⊢ ((ω
CNF 𝑐):dom (ω CNF
𝑐)–1-1-onto→(ω ↑o 𝑐) → Fun (ω CNF 𝑐)) |
| 19 | 17, 18 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑎 = 𝐴) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → Fun (ω CNF 𝑐)) |
| 20 | | funbrfvb 6962 |
. . . . . . . . . . . 12
⊢ ((Fun
(ω CNF 𝑐) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → (((ω CNF 𝑐)‘𝑓) = 𝐴 ↔ 𝑓(ω CNF 𝑐)𝐴)) |
| 21 | 19, 20 | sylancom 588 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑎 = 𝐴) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → (((ω CNF 𝑐)‘𝑓) = 𝐴 ↔ 𝑓(ω CNF 𝑐)𝐴)) |
| 22 | 11, 21 | bitr4d 282 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑎 = 𝐴) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → (𝑓(ω CNF 𝑐)𝑎 ↔ ((ω CNF 𝑐)‘𝑓) = 𝐴)) |
| 23 | 22 | reubidva 3396 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑎 = 𝐴) → (∃!𝑓 ∈ dom (ω CNF 𝑐)𝑓(ω CNF 𝑐)𝑎 ↔ ∃!𝑓 ∈ dom (ω CNF 𝑐)((ω CNF 𝑐)‘𝑓) = 𝐴)) |
| 24 | | simpl2 1193 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → 𝑏 ∈ On) |
| 25 | 13 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → ω ∈
On) |
| 26 | 24, 15, 25 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → (𝑏 ∈ On ∧ 𝑐 ∈ On ∧ ω ∈
On)) |
| 27 | | peano1 7910 |
. . . . . . . . . . . . 13
⊢ ∅
∈ ω |
| 28 | 26, 27 | jctir 520 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → ((𝑏 ∈ On ∧ 𝑐 ∈ On ∧ ω ∈ On) ∧
∅ ∈ ω)) |
| 29 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → 𝑏 ⊆ 𝑐) |
| 30 | | oewordi 8629 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ On ∧ 𝑐 ∈ On ∧ ω ∈
On) ∧ ∅ ∈ ω) → (𝑏 ⊆ 𝑐 → (ω ↑o 𝑏) ⊆ (ω
↑o 𝑐))) |
| 31 | 28, 29, 30 | sylc 65 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → (ω
↑o 𝑏)
⊆ (ω ↑o 𝑐)) |
| 32 | | simpl3 1194 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → 𝐴 ∈ (ω ↑o 𝑏)) |
| 33 | 31, 32 | sseldd 3984 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → 𝐴 ∈ (ω ↑o 𝑐)) |
| 34 | 12, 25, 15 | cantnff1o 9736 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → (ω CNF 𝑐):dom (ω CNF 𝑐)–1-1-onto→(ω ↑o 𝑐)) |
| 35 | | dff1o5 6857 |
. . . . . . . . . . . 12
⊢ ((ω
CNF 𝑐):dom (ω CNF
𝑐)–1-1-onto→(ω ↑o 𝑐) ↔ ((ω CNF 𝑐):dom (ω CNF 𝑐)–1-1→(ω ↑o 𝑐) ∧ ran (ω CNF 𝑐) = (ω ↑o 𝑐))) |
| 36 | | simpr 484 |
. . . . . . . . . . . 12
⊢
(((ω CNF 𝑐):dom (ω CNF 𝑐)–1-1→(ω ↑o 𝑐) ∧ ran (ω CNF 𝑐) = (ω ↑o 𝑐)) → ran (ω CNF 𝑐) = (ω ↑o
𝑐)) |
| 37 | 35, 36 | sylbi 217 |
. . . . . . . . . . 11
⊢ ((ω
CNF 𝑐):dom (ω CNF
𝑐)–1-1-onto→(ω ↑o 𝑐) → ran (ω CNF 𝑐) = (ω ↑o 𝑐)) |
| 38 | 34, 37 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → ran (ω CNF 𝑐) = (ω ↑o
𝑐)) |
| 39 | 33, 38 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → 𝐴 ∈ ran (ω CNF 𝑐)) |
| 40 | | dff1o2 6853 |
. . . . . . . . . . . 12
⊢ ((ω
CNF 𝑐):dom (ω CNF
𝑐)–1-1-onto→(ω ↑o 𝑐) ↔ ((ω CNF 𝑐) Fn dom (ω CNF 𝑐) ∧ Fun ◡(ω CNF 𝑐) ∧ ran (ω CNF 𝑐) = (ω ↑o 𝑐))) |
| 41 | | simp2 1138 |
. . . . . . . . . . . 12
⊢
(((ω CNF 𝑐) Fn
dom (ω CNF 𝑐) ∧
Fun ◡(ω CNF 𝑐) ∧ ran (ω CNF 𝑐) = (ω ↑o 𝑐)) → Fun ◡(ω CNF 𝑐)) |
| 42 | 40, 41 | sylbi 217 |
. . . . . . . . . . 11
⊢ ((ω
CNF 𝑐):dom (ω CNF
𝑐)–1-1-onto→(ω ↑o 𝑐) → Fun ◡(ω CNF 𝑐)) |
| 43 | 34, 42 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → Fun ◡(ω CNF 𝑐)) |
| 44 | | funcnv3 6636 |
. . . . . . . . . 10
⊢ (Fun
◡(ω CNF 𝑐) ↔ ∀𝑎 ∈ ran (ω CNF 𝑐)∃!𝑓 ∈ dom (ω CNF 𝑐)𝑓(ω CNF 𝑐)𝑎) |
| 45 | 43, 44 | sylib 218 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → ∀𝑎 ∈ ran (ω CNF 𝑐)∃!𝑓 ∈ dom (ω CNF 𝑐)𝑓(ω CNF 𝑐)𝑎) |
| 46 | 23, 39, 45 | rspcdv2 3617 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → ∃!𝑓 ∈ dom (ω CNF 𝑐)((ω CNF 𝑐)‘𝑓) = 𝐴) |
| 47 | 32 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → 𝐴 ∈ (ω ↑o 𝑏)) |
| 48 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → 𝑓 ∈ dom (ω CNF 𝑐)) |
| 49 | 13 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ω ∈ On) |
| 50 | 15 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → 𝑐 ∈ On) |
| 51 | 12, 49, 50 | cantnfs 9706 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → (𝑓 ∈ dom (ω CNF 𝑐) ↔ (𝑓:𝑐⟶ω ∧ 𝑓 finSupp ∅))) |
| 52 | 48, 51 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → (𝑓:𝑐⟶ω ∧ 𝑓 finSupp ∅)) |
| 53 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝑐⟶ω ∧ 𝑓 finSupp ∅) → 𝑓 finSupp ∅) |
| 54 | 52, 53 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → 𝑓 finSupp ∅) |
| 55 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ dom
(ω CNF 𝑏) = dom
(ω CNF 𝑏) |
| 56 | 24 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → 𝑏 ∈ On) |
| 57 | 29 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → 𝑏 ⊆ 𝑐) |
| 58 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ((ω CNF 𝑐)‘𝑓) = 𝐴) |
| 59 | 58, 47 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ((ω CNF 𝑐)‘𝑓) ∈ (ω ↑o 𝑏)) |
| 60 | | 1onn 8678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
1o ∈ ω |
| 61 | | ondif2 8540 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ω
∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o
∈ ω)) |
| 62 | 13, 60, 61 | mpbir2an 711 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ω
∈ (On ∖ 2o) |
| 63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ω ∈ (On ∖
2o)) |
| 64 | | cantnfresb 43337 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ω ∈ (On ∖ 2o) ∧ 𝑐 ∈ On) ∧ (𝑏 ∈ On ∧ 𝑓 ∈ dom (ω CNF 𝑐))) → (((ω CNF 𝑐)‘𝑓) ∈ (ω ↑o 𝑏) ↔ ∀𝑑 ∈ (𝑐 ∖ 𝑏)(𝑓‘𝑑) = ∅)) |
| 65 | 63, 50, 56, 48, 64 | syl22anc 839 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → (((ω CNF 𝑐)‘𝑓) ∈ (ω ↑o 𝑏) ↔ ∀𝑑 ∈ (𝑐 ∖ 𝑏)(𝑓‘𝑑) = ∅)) |
| 66 | 59, 65 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ∀𝑑 ∈ (𝑐 ∖ 𝑏)(𝑓‘𝑑) = ∅) |
| 67 | 66 | r19.21bi 3251 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) ∧ 𝑑 ∈ (𝑐 ∖ 𝑏)) → (𝑓‘𝑑) = ∅) |
| 68 | 27 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ∅ ∈
ω) |
| 69 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) ∧ 𝑑 ∈ 𝑏) → 𝑓 ∈ dom (ω CNF 𝑐)) |
| 70 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) ∧ 𝑑 ∈ 𝑏) → ω ∈ On) |
| 71 | 15 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → 𝑐 ∈ On) |
| 72 | 71 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) ∧ 𝑑 ∈ 𝑏) → 𝑐 ∈ On) |
| 73 | 12, 70, 72 | cantnfs 9706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) ∧ 𝑑 ∈ 𝑏) → (𝑓 ∈ dom (ω CNF 𝑐) ↔ (𝑓:𝑐⟶ω ∧ 𝑓 finSupp ∅))) |
| 74 | 69, 73 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) ∧ 𝑑 ∈ 𝑏) → (𝑓:𝑐⟶ω ∧ 𝑓 finSupp ∅)) |
| 75 | 74 | simpld 494 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) ∧ 𝑑 ∈ 𝑏) → 𝑓:𝑐⟶ω) |
| 76 | 57 | sselda 3983 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) ∧ 𝑑 ∈ 𝑏) → 𝑑 ∈ 𝑐) |
| 77 | 75, 76 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) ∧ 𝑑 ∈ 𝑏) → (𝑓‘𝑑) ∈ ω) |
| 78 | 77 | fmpttd 7135 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → (𝑑 ∈ 𝑏 ↦ (𝑓‘𝑑)):𝑏⟶ω) |
| 79 | 12, 25, 15 | cantnfs 9706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → (𝑓 ∈ dom (ω CNF 𝑐) ↔ (𝑓:𝑐⟶ω ∧ 𝑓 finSupp ∅))) |
| 80 | 79 | simprbda 498 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → 𝑓:𝑐⟶ω) |
| 81 | 80 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → 𝑓:𝑐⟶ω) |
| 82 | 81, 57 | feqresmpt 6978 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → (𝑓 ↾ 𝑏) = (𝑑 ∈ 𝑏 ↦ (𝑓‘𝑑))) |
| 83 | 54, 68 | fsuppres 9433 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → (𝑓 ↾ 𝑏) finSupp ∅) |
| 84 | 82, 83 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → (𝑑 ∈ 𝑏 ↦ (𝑓‘𝑑)) finSupp ∅) |
| 85 | 55, 49, 56 | cantnfs 9706 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ((𝑑 ∈ 𝑏 ↦ (𝑓‘𝑑)) ∈ dom (ω CNF 𝑏) ↔ ((𝑑 ∈ 𝑏 ↦ (𝑓‘𝑑)):𝑏⟶ω ∧ (𝑑 ∈ 𝑏 ↦ (𝑓‘𝑑)) finSupp ∅))) |
| 86 | 78, 84, 85 | mpbir2and 713 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → (𝑑 ∈ 𝑏 ↦ (𝑓‘𝑑)) ∈ dom (ω CNF 𝑏)) |
| 87 | 55, 49, 56, 50, 57, 67, 68, 12, 86 | cantnfres 9717 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ((ω CNF 𝑏)‘(𝑑 ∈ 𝑏 ↦ (𝑓‘𝑑))) = ((ω CNF 𝑐)‘(𝑑 ∈ 𝑐 ↦ (𝑓‘𝑑)))) |
| 88 | 82 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = ((ω CNF 𝑏)‘(𝑑 ∈ 𝑏 ↦ (𝑓‘𝑑)))) |
| 89 | 81 | feqmptd 6977 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → 𝑓 = (𝑑 ∈ 𝑐 ↦ (𝑓‘𝑑))) |
| 90 | 89 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ((ω CNF 𝑐)‘𝑓) = ((ω CNF 𝑐)‘(𝑑 ∈ 𝑐 ↦ (𝑓‘𝑑)))) |
| 91 | 87, 88, 90 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = ((ω CNF 𝑐)‘𝑓)) |
| 92 | 91, 58 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → ((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴) |
| 93 | 47, 54, 92 | 3jca 1129 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ On
∧ 𝑏 ∈ On ∧
𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) → (𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅ ∧ ((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴)) |
| 94 | 93 | ex 412 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → (((ω CNF 𝑐)‘𝑓) = 𝐴 → (𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅ ∧ ((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴))) |
| 95 | 94 | pm4.71rd 562 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → (((ω CNF 𝑐)‘𝑓) = 𝐴 ↔ ((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅ ∧ ((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴))) |
| 96 | | 3an4anass 1105 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (ω
↑o 𝑏) ∧
𝑓 finSupp ∅ ∧
((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴) ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴) ↔ ((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴))) |
| 97 | 95, 96 | bitrdi 287 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) ∧ 𝑓 ∈ dom (ω CNF 𝑐)) → (((ω CNF 𝑐)‘𝑓) = 𝐴 ↔ ((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴)))) |
| 98 | 97 | reubidva 3396 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → (∃!𝑓 ∈ dom (ω CNF 𝑐)((ω CNF 𝑐)‘𝑓) = 𝐴 ↔ ∃!𝑓 ∈ dom (ω CNF 𝑐)((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴)))) |
| 99 | 46, 98 | mpbid 232 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
∧ (𝑐 ∈ On ∧
𝑏 ⊆ 𝑐)) → ∃!𝑓 ∈ dom (ω CNF 𝑐)((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴))) |
| 100 | 99 | ex 412 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
→ ((𝑐 ∈ On ∧
𝑏 ⊆ 𝑐) → ∃!𝑓 ∈ dom (ω CNF 𝑐)((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴)))) |
| 101 | 9, 100 | sylbid 240 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
→ (𝑐 ∈ (On
∖ 𝑏) →
∃!𝑓 ∈ dom
(ω CNF 𝑐)((𝐴 ∈ (ω
↑o 𝑏) ∧
𝑓 finSupp ∅) ∧
(((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴)))) |
| 102 | 101 | ralrimiv 3145 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ On ∧ 𝐴 ∈ (ω
↑o 𝑏))
→ ∀𝑐 ∈ (On
∖ 𝑏)∃!𝑓 ∈ dom (ω CNF 𝑐)((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴))) |
| 103 | 102 | 3exp 1120 |
. . 3
⊢ (𝐴 ∈ On → (𝑏 ∈ On → (𝐴 ∈ (ω
↑o 𝑏)
→ ∀𝑐 ∈ (On
∖ 𝑏)∃!𝑓 ∈ dom (ω CNF 𝑐)((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴))))) |
| 104 | 103 | reximdvai 3165 |
. 2
⊢ (𝐴 ∈ On → (∃𝑏 ∈ On 𝐴 ∈ (ω ↑o 𝑏) → ∃𝑏 ∈ On ∀𝑐 ∈ (On ∖ 𝑏)∃!𝑓 ∈ dom (ω CNF 𝑐)((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴)))) |
| 105 | 1, 104 | mpd 15 |
1
⊢ (𝐴 ∈ On → ∃𝑏 ∈ On ∀𝑐 ∈ (On ∖ 𝑏)∃!𝑓 ∈ dom (ω CNF 𝑐)((𝐴 ∈ (ω ↑o 𝑏) ∧ 𝑓 finSupp ∅) ∧ (((ω CNF 𝑏)‘(𝑓 ↾ 𝑏)) = 𝐴 ∧ ((ω CNF 𝑐)‘𝑓) = 𝐴))) |