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

Metamath Proof Explorer

Theorem axprOLD

Description: Obsolete version of axpr as of 18-Sep-2025. (Contributed by NM, 14-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axprOLD 
|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )

Proof

Step Hyp Ref Expression
1 axprlem3OLD 
 |-  E. z A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )
2 biimpr 
 |-  ( ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z ) )
3 2 alimi 
 |-  ( A. w ( w e. z <-> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) -> A. w ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z ) )
4 1 3 eximii 
 |-  E. z A. w ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z )
5 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 ) ) )
6 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 ) ) )
7 5 6 jaodan 
 |-  ( ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) /\ ( w = x \/ w = y ) ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) )
8 7 ex 
 |-  ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( ( w = x \/ w = y ) -> E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) ) )
9 8 imim1d 
 |-  ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z ) -> ( ( w = x \/ w = y ) -> w e. z ) ) )
10 9 alimdv 
 |-  ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( A. w ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z ) -> A. w ( ( w = x \/ w = y ) -> w e. z ) ) )
11 10 eximdv 
 |-  ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> ( E. z A. w ( E. s ( s e. p /\ if- ( E. n n e. s , w = x , w = y ) ) -> w e. z ) -> E. z A. w ( ( w = x \/ w = y ) -> w e. z ) ) )
12 4 11 mpi 
 |-  ( A. s ( A. n e. s A. t -. t e. n -> s e. p ) -> E. z A. w ( ( w = x \/ w = y ) -> w e. z ) )
13 axprlem2 
 |-  E. p A. s ( A. n e. s A. t -. t e. n -> s e. p )
14 12 13 exlimiiv 
 |-  E. z A. w ( ( w = x \/ w = y ) -> w e. z )