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

Metamath Proof Explorer

Theorem axprlem5OLD

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 axprlem5OLD 
|- ( ( 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 ) ) )