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

Proof

Step Hyp Ref Expression
1 axprlem1 
 |-  E. s A. n ( A. t -. t e. n -> n e. s )
2 1 bm1.3ii 
 |-  E. s A. n ( n e. s <-> A. t -. t e. n )
3 nfa1 
 |-  F/ s A. s ( A. n e. s A. t -. t e. n -> s e. p )
4 nfv 
 |-  F/ s w = x
5 3 4 nfan 
 |-  F/ s ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = x )
6 biimp 
 |-  ( ( n e. s <-> A. t -. t e. n ) -> ( n e. s -> A. t -. t e. n ) )
7 6 alimi 
 |-  ( A. n ( n e. s <-> A. t -. t e. n ) -> 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. t -. t e. n ) -> 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 9 10 mpan9 
 |-  ( ( A. n ( n e. s <-> A. t -. t e. n ) /\ A. s ( A. n e. s A. t -. t e. n -> s e. p ) ) -> s e. p )
12 11 adantrr 
 |-  ( ( A. n ( n e. s <-> A. t -. t e. n ) /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = x ) ) -> s e. p )
13 ax-nul 
 |-  E. n A. t -. t e. n
14 nfa1 
 |-  F/ n A. n ( n e. s <-> A. t -. t e. n )
15 sp 
 |-  ( A. n ( n e. s <-> A. t -. t e. n ) -> ( n e. s <-> A. t -. t e. n ) )
16 15 biimprd 
 |-  ( A. n ( n e. s <-> A. t -. t e. n ) -> ( A. t -. t e. n -> n e. s ) )
17 14 16 eximd 
 |-  ( A. n ( n e. s <-> A. t -. t e. n ) -> ( E. n A. t -. t e. n -> E. n n e. s ) )
18 13 17 mpi 
 |-  ( A. n ( n e. s <-> A. t -. t e. n ) -> E. n n e. s )
19 simprr 
 |-  ( ( A. n ( n e. s <-> A. t -. t e. n ) /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = x ) ) -> w = x )
20 ifptru 
 |-  ( E. n n e. s -> ( if- ( E. n n e. s , w = x , w = y ) <-> w = x ) )
21 20 biimpar 
 |-  ( ( E. n n e. s /\ w = x ) -> if- ( E. n n e. s , w = x , w = y ) )
22 18 19 21 syl2an2r 
 |-  ( ( A. n ( n e. s <-> A. t -. t e. n ) /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = x ) ) -> if- ( E. n n e. s , w = x , w = y ) )
23 12 22 jca 
 |-  ( ( A. n ( n e. s <-> A. t -. t e. n ) /\ ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = x ) ) -> ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )
24 23 expcom 
 |-  ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = x ) -> ( A. n ( n e. s <-> A. t -. t e. n ) -> ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) )
25 5 24 eximd 
 |-  ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = x ) -> ( E. s A. n ( n e. s <-> A. t -. t e. n ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) )
26 2 25 mpi 
 |-  ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ w = x ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )