Metamath Proof Explorer

Theorem axprlem4

Description: Lemma for axpr . The first 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 axprlem4 ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=x→∃ss∈p∧if-∃nn∈sw=xw=y

Proof

Step Hyp Ref Expression
1 axprlem1 ⊢∃s∀n∀t¬t∈n→n∈s
2 1 bm1.3ii ⊢∃s∀nn∈s↔∀t¬t∈n
3 nfa1 ⊢Ⅎs∀s∀n∈s∀t¬t∈n→s∈p
4 nfv ⊢Ⅎsw=x
5 3 4 nfan ⊢Ⅎs∀s∀n∈s∀t¬t∈n→s∈p∧w=x
6 biimp ⊢n∈s↔∀t¬t∈n→n∈s→∀t¬t∈n
7 6 alimi ⊢∀nn∈s↔∀t¬t∈n→∀nn∈s→∀t¬t∈n
8 df-ral ⊢∀n∈s∀t¬t∈n↔∀nn∈s→∀t¬t∈n
9 7 8 sylibr ⊢∀nn∈s↔∀t¬t∈n→∀n∈s∀t¬t∈n
10 sp ⊢∀s∀n∈s∀t¬t∈n→s∈p→∀n∈s∀t¬t∈n→s∈p
11 9 10 mpan9 ⊢∀nn∈s↔∀t¬t∈n∧∀s∀n∈s∀t¬t∈n→s∈p→s∈p
12 11 adantrr ⊢∀nn∈s↔∀t¬t∈n∧∀s∀n∈s∀t¬t∈n→s∈p∧w=x→s∈p
13 ax-nul ⊢∃n∀t¬t∈n
14 nfa1 ⊢Ⅎn∀nn∈s↔∀t¬t∈n
15 sp ⊢∀nn∈s↔∀t¬t∈n→n∈s↔∀t¬t∈n
16 15 biimprd ⊢∀nn∈s↔∀t¬t∈n→∀t¬t∈n→n∈s
17 14 16 eximd ⊢∀nn∈s↔∀t¬t∈n→∃n∀t¬t∈n→∃nn∈s
18 13 17 mpi ⊢∀nn∈s↔∀t¬t∈n→∃nn∈s
19 simprr ⊢∀nn∈s↔∀t¬t∈n∧∀s∀n∈s∀t¬t∈n→s∈p∧w=x→w=x
20 ifptru ⊢∃nn∈s→if-∃nn∈sw=xw=y↔w=x
21 20 biimpar ⊢∃nn∈s∧w=x→if-∃nn∈sw=xw=y
22 18 19 21 syl2an2r ⊢∀nn∈s↔∀t¬t∈n∧∀s∀n∈s∀t¬t∈n→s∈p∧w=x→if-∃nn∈sw=xw=y
23 12 22 jca ⊢∀nn∈s↔∀t¬t∈n∧∀s∀n∈s∀t¬t∈n→s∈p∧w=x→s∈p∧if-∃nn∈sw=xw=y
24 23 expcom ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=x→∀nn∈s↔∀t¬t∈n→s∈p∧if-∃nn∈sw=xw=y
25 5 24 eximd ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=x→∃s∀nn∈s↔∀t¬t∈n→∃ss∈p∧if-∃nn∈sw=xw=y
26 2 25 mpi ⊢∀s∀n∈s∀t¬t∈n→s∈p∧w=x→∃ss∈p∧if-∃nn∈sw=xw=y