Metamath Proof Explorer

Theorem axprlem4

Description: Lemma for axpr . 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
Hypotheses axprlem4.1 ⊢ ∃ s ∀ n φ
axprlem4.2 ⊢ φ → n ∈ s → ∀ t ¬ t ∈ n
axprlem4.3 ⊢ ∀ n φ → if- ∃ n n ∈ s w = x w = y ↔ w = v
Assertion axprlem4 ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → w = v → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y

Proof

Step Hyp Ref Expression
1 axprlem4.1 ⊢ ∃ s ∀ n φ
2 axprlem4.2 ⊢ φ → n ∈ s → ∀ t ¬ t ∈ n
3 axprlem4.3 ⊢ ∀ n φ → if- ∃ n n ∈ s w = x w = y ↔ w = v
4 2 alimi ⊢ ∀ n φ → ∀ n n ∈ s → ∀ t ¬ t ∈ n
5 df-ral ⊢ ∀ n ∈ s ∀ t ¬ t ∈ n ↔ ∀ n n ∈ s → ∀ t ¬ t ∈ n
6 4 5 sylibr ⊢ ∀ n φ → ∀ n ∈ s ∀ t ¬ t ∈ n
7 6 imim1i ⊢ ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∀ n φ → s ∈ p
8 7 ancrd ⊢ ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∀ n φ → s ∈ p ∧ ∀ n φ
9 8 aleximi ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∃ s ∀ n φ → ∃ s s ∈ p ∧ ∀ n φ
10 1 9 mpi ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∃ s s ∈ p ∧ ∀ n φ
11 3 biimprcd ⊢ w = v → ∀ n φ → if- ∃ n n ∈ s w = x w = y
12 11 anim2d ⊢ w = v → s ∈ p ∧ ∀ n φ → s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
13 12 eximdv ⊢ w = v → ∃ s s ∈ p ∧ ∀ n φ → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
14 10 13 syl5com ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → w = v → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y