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

Metamath Proof Explorer

Theorem axprlem2

Description: Lemma for axpr . There exists a set to which all sets whose only members are empty sets belong. (Contributed by Rohan Ridenour, 9-Aug-2023) (Revised by BJ, 13-Aug-2023)

Ref Expression
Assertion axprlem2 
|- E. x A. y ( A. z e. y A. w -. w e. z -> y e. x )

Proof

Step Hyp Ref Expression
1 ax-pow 
 |-  E. x A. y ( A. z ( z e. y -> z e. v ) -> y e. x )
2 df-ral 
 |-  ( A. z e. y A. w -. w e. z <-> A. z ( z e. y -> A. w -. w e. z ) )
3 imim2 
 |-  ( ( A. w -. w e. z -> z e. v ) -> ( ( z e. y -> A. w -. w e. z ) -> ( z e. y -> z e. v ) ) )
4 3 al2imi 
 |-  ( A. z ( A. w -. w e. z -> z e. v ) -> ( A. z ( z e. y -> A. w -. w e. z ) -> A. z ( z e. y -> z e. v ) ) )
5 2 4 biimtrid 
 |-  ( A. z ( A. w -. w e. z -> z e. v ) -> ( A. z e. y A. w -. w e. z -> A. z ( z e. y -> z e. v ) ) )
6 5 imim1d 
 |-  ( A. z ( A. w -. w e. z -> z e. v ) -> ( ( A. z ( z e. y -> z e. v ) -> y e. x ) -> ( A. z e. y A. w -. w e. z -> y e. x ) ) )
7 6 alimdv 
 |-  ( A. z ( A. w -. w e. z -> z e. v ) -> ( A. y ( A. z ( z e. y -> z e. v ) -> y e. x ) -> A. y ( A. z e. y A. w -. w e. z -> y e. x ) ) )
8 7 eximdv 
 |-  ( A. z ( A. w -. w e. z -> z e. v ) -> ( E. x A. y ( A. z ( z e. y -> z e. v ) -> y e. x ) -> E. x A. y ( A. z e. y A. w -. w e. z -> y e. x ) ) )
9 1 8 mpi 
 |-  ( A. z ( A. w -. w e. z -> z e. v ) -> E. x A. y ( A. z e. y A. w -. w e. z -> y e. x ) )
10 axprlem1 
 |-  E. v A. z ( A. w -. w e. z -> z e. v )
11 9 10 exlimiiv 
 |-  E. x A. y ( A. z e. y A. w -. w e. z -> y e. x )