This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axprlem4OLD

Description: Obsolete version of axprlem4 as of 18-Sep-2025. (Contributed by Rohan Ridenour, 10-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axprlem4OLD 
|- ( ( 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.3iiOLD 
 |-  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 ) ) )