Proof of Theorem cofonr
| Step | Hyp | Ref
| Expression |
| 1 | | cofonr.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ On) |
| 2 | | onss 7805 |
. . . . . . . 8
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
| 3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ On) |
| 4 | 3 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ On) |
| 5 | | eloni 6394 |
. . . . . 6
⊢ (𝑦 ∈ On → Ord 𝑦) |
| 6 | | ordirr 6402 |
. . . . . 6
⊢ (Ord
𝑦 → ¬ 𝑦 ∈ 𝑦) |
| 7 | 4, 5, 6 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦 ∈ 𝑦) |
| 8 | | cofonr.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥}) |
| 9 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥}) |
| 10 | 9 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ⊆ 𝑦) → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥}) |
| 11 | 4 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ⊆ 𝑦) → 𝑦 ∈ On) |
| 12 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ⊆ 𝑦) → 𝑋 ⊆ 𝑦) |
| 13 | | sseq2 4010 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑋 ⊆ 𝑥 ↔ 𝑋 ⊆ 𝑦)) |
| 14 | 13 | elrab 3692 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ↔ (𝑦 ∈ On ∧ 𝑋 ⊆ 𝑦)) |
| 15 | 11, 12, 14 | sylanbrc 583 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ⊆ 𝑦) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥}) |
| 16 | | intss1 4963 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} → ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ⊆ 𝑦) |
| 17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ⊆ 𝑦) → ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥} ⊆ 𝑦) |
| 18 | 10, 17 | eqsstrd 4018 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ⊆ 𝑦) → 𝐴 ⊆ 𝑦) |
| 19 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ⊆ 𝑦) → 𝑦 ∈ 𝐴) |
| 20 | 18, 19 | sseldd 3984 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑋 ⊆ 𝑦) → 𝑦 ∈ 𝑦) |
| 21 | 7, 20 | mtand 816 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑋 ⊆ 𝑦) |
| 22 | | dfss3 3972 |
. . . 4
⊢ (𝑋 ⊆ 𝑦 ↔ ∀𝑧 ∈ 𝑋 𝑧 ∈ 𝑦) |
| 23 | 21, 22 | sylnib 328 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ¬ ∀𝑧 ∈ 𝑋 𝑧 ∈ 𝑦) |
| 24 | 8, 1 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝜑 → ∩ {𝑥
∈ On ∣ 𝑋 ⊆
𝑥} ∈
On) |
| 25 | | onintrab2 7817 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈ On
𝑋 ⊆ 𝑥 ↔ ∩ {𝑥
∈ On ∣ 𝑋 ⊆
𝑥} ∈
On) |
| 26 | 24, 25 | sylibr 234 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑥 ∈ On 𝑋 ⊆ 𝑥) |
| 27 | 26 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∃𝑥 ∈ On 𝑋 ⊆ 𝑥) |
| 28 | | onss 7805 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → 𝑥 ⊆ On) |
| 29 | 28 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ On) → 𝑥 ⊆ On) |
| 30 | | sstr 3992 |
. . . . . . . . . . 11
⊢ ((𝑋 ⊆ 𝑥 ∧ 𝑥 ⊆ On) → 𝑋 ⊆ On) |
| 31 | 30 | expcom 413 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ On → (𝑋 ⊆ 𝑥 → 𝑋 ⊆ On)) |
| 32 | 29, 31 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ∈ On) → (𝑋 ⊆ 𝑥 → 𝑋 ⊆ On)) |
| 33 | 32 | rexlimdva 3155 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (∃𝑥 ∈ On 𝑋 ⊆ 𝑥 → 𝑋 ⊆ On)) |
| 34 | 27, 33 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑋 ⊆ On) |
| 35 | 34 | sselda 3983 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ On) |
| 36 | | ontri1 6418 |
. . . . . 6
⊢ ((𝑦 ∈ On ∧ 𝑧 ∈ On) → (𝑦 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑦)) |
| 37 | 4, 35, 36 | syl2an2r 685 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝑋) → (𝑦 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑦)) |
| 38 | 37 | rexbidva 3177 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (∃𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝑋 ¬ 𝑧 ∈ 𝑦)) |
| 39 | | rexnal 3100 |
. . . 4
⊢
(∃𝑧 ∈
𝑋 ¬ 𝑧 ∈ 𝑦 ↔ ¬ ∀𝑧 ∈ 𝑋 𝑧 ∈ 𝑦) |
| 40 | 38, 39 | bitrdi 287 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (∃𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧 ↔ ¬ ∀𝑧 ∈ 𝑋 𝑧 ∈ 𝑦)) |
| 41 | 23, 40 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∃𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧) |
| 42 | 41 | ralrimiva 3146 |
1
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧) |