Metamath Proof Explorer

Theorem axprlem5

Description: Lemma for axpr . The second element of the pair 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)

Ref Expression
Assertion axprlem5 ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=y→∃ss∈p∧if-∃nn∈sw=xw=y

Proof

Step Hyp Ref Expression
1 ax-nul ⊢∃s∀n¬n∈s
2 nfa1 ⊢Ⅎs∀s∀n∈s∀t¬t∈n→s∈p
3 nfv ⊢Ⅎsw=y
4 2 3 nfan ⊢Ⅎs∀s∀n∈s∀t¬t∈n→s∈p∧w=y
5 pm2.21 ⊢¬n∈s→n∈s→∀t¬t∈n
6 5 alimi ⊢∀n¬n∈s→∀nn∈s→∀t¬t∈n
7 6 adantr ⊢∀n¬n∈s∧∀s∀n∈s∀t¬t∈n→s∈p∧w=y→∀nn∈s→∀t¬t∈n
8 df-ral ⊢∀n∈s∀t¬t∈n↔∀nn∈s→∀t¬t∈n
9 7 8 sylibr ⊢∀n¬n∈s∧∀s∀n∈s∀t¬t∈n→s∈p∧w=y→∀n∈s∀t¬t∈n
10 sp ⊢∀s∀n∈s∀t¬t∈n→s∈p→∀n∈s∀t¬t∈n→s∈p
11 10 ad2antrl ⊢∀n¬n∈s∧∀s∀n∈s∀t¬t∈n→s∈p∧w=y→∀n∈s∀t¬t∈n→s∈p
12 9 11 mpd ⊢∀n¬n∈s∧∀s∀n∈s∀t¬t∈n→s∈p∧w=y→s∈p
13 simpl ⊢∀n¬n∈s∧∀s∀n∈s∀t¬t∈n→s∈p∧w=y→∀n¬n∈s
14 alnex ⊢∀n¬n∈s↔¬∃nn∈s
15 13 14 sylib ⊢∀n¬n∈s∧∀s∀n∈s∀t¬t∈n→s∈p∧w=y→¬∃nn∈s
16 simprr ⊢∀n¬n∈s∧∀s∀n∈s∀t¬t∈n→s∈p∧w=y→w=y
17 ifpfal ⊢¬∃nn∈s→if-∃nn∈sw=xw=y↔w=y
18 17 biimpar ⊢¬∃nn∈s∧w=y→if-∃nn∈sw=xw=y
19 15 16 18 syl2anc ⊢∀n¬n∈s∧∀s∀n∈s∀t¬t∈n→s∈p∧w=y→if-∃nn∈sw=xw=y
20 12 19 jca ⊢∀n¬n∈s∧∀s∀n∈s∀t¬t∈n→s∈p∧w=y→s∈p∧if-∃nn∈sw=xw=y
21 20 expcom ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=y→∀n¬n∈s→s∈p∧if-∃nn∈sw=xw=y
22 4 21 eximd ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=y→∃s∀n¬n∈s→∃ss∈p∧if-∃nn∈sw=xw=y
23 1 22 mpi ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=y→∃ss∈p∧if-∃nn∈sw=xw=y