| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > axprlem4 | Structured version Visualization version GIF version | ||
| Description: Lemma for axpr 5427. If an existing set of empty sets corresponds to one element of the pair, then the element is included in any superset of the set whose existence is asserted by the axiom of replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, 13-Aug-2023.) (Revised by Matthew House, 18-Sep-2025.) |
| Ref | Expression |
|---|---|
| axprlem4.1 | ⊢ ∃𝑠∀𝑛𝜑 |
| axprlem4.2 | ⊢ (𝜑 → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛)) |
| axprlem4.3 | ⊢ (∀𝑛𝜑 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑣)) |
| Ref | Expression |
|---|---|
| axprlem4 | ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (𝑤 = 𝑣 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axprlem4.1 | . . 3 ⊢ ∃𝑠∀𝑛𝜑 | |
| 2 | axprlem4.2 | . . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛)) | |
| 3 | 2 | alimi 1811 | . . . . . . 7 ⊢ (∀𝑛𝜑 → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛)) |
| 4 | df-ral 3062 | . . . . . . 7 ⊢ (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 ↔ ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛)) | |
| 5 | 3, 4 | sylibr 234 | . . . . . 6 ⊢ (∀𝑛𝜑 → ∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛) |
| 6 | 5 | imim1i 63 | . . . . 5 ⊢ ((∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛𝜑 → 𝑠 ∈ 𝑝)) |
| 7 | 6 | ancrd 551 | . . . 4 ⊢ ((∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛𝜑 → (𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑))) |
| 8 | 7 | aleximi 1832 | . . 3 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∃𝑠∀𝑛𝜑 → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑))) |
| 9 | 1, 8 | mpi 20 | . 2 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑)) |
| 10 | axprlem4.3 | . . . . 5 ⊢ (∀𝑛𝜑 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑣)) | |
| 11 | 10 | biimprcd 250 | . . . 4 ⊢ (𝑤 = 𝑣 → (∀𝑛𝜑 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) |
| 12 | 11 | anim2d 612 | . . 3 ⊢ (𝑤 = 𝑣 → ((𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑) → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))) |
| 13 | 12 | eximdv 1917 | . 2 ⊢ (𝑤 = 𝑣 → (∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))) |
| 14 | 9, 13 | syl5com 31 | 1 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (𝑤 = 𝑣 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 if-wif 1063 ∀wal 1538 ∃wex 1779 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-ral 3062 |
| This theorem is referenced by: axpr 5427 |
| Copyright terms: Public domain | W3C validator |