Proof of Theorem axprlem4OLD
| Step | Hyp | Ref
| Expression |
| 1 | | axprlem1 5421 |
. . 3
⊢
∃𝑠∀𝑛(∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑛 ∈ 𝑠) |
| 2 | 1 | bm1.3iiOLD 5300 |
. 2
⊢
∃𝑠∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) |
| 3 | | nfa1 2151 |
. . . 4
⊢
Ⅎ𝑠∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) |
| 4 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑠 𝑤 = 𝑥 |
| 5 | 3, 4 | nfan 1899 |
. . 3
⊢
Ⅎ𝑠(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥) |
| 6 | | biimp 215 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛)) |
| 7 | 6 | alimi 1811 |
. . . . . . . 8
⊢
(∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛)) |
| 8 | | df-ral 3061 |
. . . . . . . 8
⊢
(∀𝑛 ∈
𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 ↔ ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛)) |
| 9 | 7, 8 | sylibr 234 |
. . . . . . 7
⊢
(∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → ∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛) |
| 10 | | sp 2183 |
. . . . . . 7
⊢
(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝)) |
| 11 | 9, 10 | mpan9 506 |
. . . . . 6
⊢
((∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) ∧ ∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝)) → 𝑠 ∈ 𝑝) |
| 12 | 11 | adantrr 717 |
. . . . 5
⊢
((∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥)) → 𝑠 ∈ 𝑝) |
| 13 | | ax-nul 5304 |
. . . . . . 7
⊢
∃𝑛∀𝑡 ¬ 𝑡 ∈ 𝑛 |
| 14 | | nfa1 2151 |
. . . . . . . 8
⊢
Ⅎ𝑛∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) |
| 15 | | sp 2183 |
. . . . . . . . 9
⊢
(∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛)) |
| 16 | 15 | biimprd 248 |
. . . . . . . 8
⊢
(∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑛 ∈ 𝑠)) |
| 17 | 14, 16 | eximd 2216 |
. . . . . . 7
⊢
(∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (∃𝑛∀𝑡 ¬ 𝑡 ∈ 𝑛 → ∃𝑛 𝑛 ∈ 𝑠)) |
| 18 | 13, 17 | mpi 20 |
. . . . . 6
⊢
(∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → ∃𝑛 𝑛 ∈ 𝑠) |
| 19 | | simprr 773 |
. . . . . 6
⊢
((∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑥) |
| 20 | | ifptru 1075 |
. . . . . . 7
⊢
(∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥)) |
| 21 | 20 | biimpar 477 |
. . . . . 6
⊢
((∃𝑛 𝑛 ∈ 𝑠 ∧ 𝑤 = 𝑥) → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)) |
| 22 | 18, 19, 21 | syl2an2r 685 |
. . . . 5
⊢
((∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥)) → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)) |
| 23 | 12, 22 | jca 511 |
. . . 4
⊢
((∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥)) → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) |
| 24 | 23 | expcom 413 |
. . 3
⊢
((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥) → (∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))) |
| 25 | 5, 24 | eximd 2216 |
. 2
⊢
((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥) → (∃𝑠∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))) |
| 26 | 2, 25 | mpi 20 |
1
⊢
((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) |