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 
|- ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )

Proof

Step Hyp Ref Expression
1 ax-nul 
 |-  E. s A. n -. n e. s
2 nfa1 
 |-  F/ s A. s ( A. n e. s A. t -. t e. n -> s e. p )
3 nfv 
 |-  F/ s w = y
4 2 3 nfan 
 |-  F/ s ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y )
5 pm2.21 
 |-  ( -. n e. s -> ( n e. s -> A. t -. t e. n ) )
6 5 alimi 
 |-  ( A. n -. n e. s -> A. n ( n e. s -> A. t -. t e. n ) )
7 6 adantr 
 |-  ( ( A. n -. n e. s /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) ) -> A. n ( n e. s -> A. t -. t e. n ) )
8 df-ral 
 |-  ( A. n e. s A. t -. t e. n <-> A. n ( n e. s -> A. t -. t e. n ) )
9 7 8 sylibr 
 |-  ( ( A. n -. n e. s /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) ) -> A. n e. s A. t -. t e. n )
10 sp 
 |-  ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( A. n e. s A. t -. t e. n -> s e. p ) )
11 10 ad2antrl 
 |-  ( ( A. n -. n e. s /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) ) -> ( A. n e. s A. t -. t e. n -> s e. p ) )
12 9 11 mpd 
 |-  ( ( A. n -. n e. s /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) ) -> s e. p )
13 simpl 
 |-  ( ( A. n -. n e. s /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) ) -> A. n -. n e. s )
14 alnex 
 |-  ( A. n -. n e. s <-> -. E. n n e. s )
15 13 14 sylib 
 |-  ( ( A. n -. n e. s /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) ) -> -. E. n n e. s )
16 simprr 
 |-  ( ( A. n -. n e. s /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) ) -> w = y )
17 ifpfal 
 |-  ( -. E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = y ) )
18 17 biimpar 
 |-  ( ( -. E. n n e. s /\ w = y ) -> if- ( E. n n e. s , w = x , w = y ) )
19 15 16 18 syl2anc 
 |-  ( ( A. n -. n e. s /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) ) -> if- ( E. n n e. s , w = x , w = y ) )
20 12 19 jca 
 |-  ( ( A. n -. n e. s /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) ) -> ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )
21 20 expcom 
 |-  ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) -> ( A. n -. n e. s -> ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) )
22 4 21 eximd 
 |-  ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) -> ( E. s A. n -. n e. s -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) )
23 1 22 mpi 
 |-  ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = y ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )