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

Metamath Proof Explorer

Theorem axprglem

Description: Lemma for axprg . (Contributed by GG, 11-Mar-2026)

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

Proof

Step Hyp Ref Expression
1 iseqsetv-clel 
 |-  ( E. y y = B <-> E. w w = B )
2 ax-pr 
 |-  E. z A. w ( ( w = x \/ w = y ) -> w e. z )
3 eqtr3 
 |-  ( ( w = B /\ y = B ) -> w = y )
4 3 expcom 
 |-  ( y = B -> ( w = B -> w = y ) )
5 4 orim2d 
 |-  ( y = B -> ( ( w = x \/ w = B ) -> ( w = x \/ w = y ) ) )
6 5 imim1d 
 |-  ( y = B -> ( ( ( w = x \/ w = y ) -> w e. z ) -> ( ( w = x \/ w = B ) -> w e. z ) ) )
7 6 alimdv 
 |-  ( y = B -> ( A. w ( ( w = x \/ w = y ) -> w e. z ) -> A. w ( ( w = x \/ w = B ) -> w e. z ) ) )
8 7 eximdv 
 |-  ( y = B -> ( E. z A. w ( ( w = x \/ w = y ) -> w e. z ) -> E. z A. w ( ( w = x \/ w = B ) -> w e. z ) ) )
9 2 8 mpi 
 |-  ( y = B -> E. z A. w ( ( w = x \/ w = B ) -> w e. z ) )
10 9 exlimiv 
 |-  ( E. y y = B -> E. z A. w ( ( w = x \/ w = B ) -> w e. z ) )
11 1 10 sylbir 
 |-  ( E. w w = B -> E. z A. w ( ( w = x \/ w = B ) -> w e. z ) )
12 ax-pr 
 |-  E. z A. w ( ( w = x \/ w = x ) -> w e. z )
13 alnex 
 |-  ( A. w -. w = B <-> -. E. w w = B )
14 orel2 
 |-  ( -. w = B -> ( ( w = x \/ w = B ) -> w = x ) )
15 pm2.67-2 
 |-  ( ( ( w = x \/ w = x ) -> w e. z ) -> ( w = x -> w e. z ) )
16 14 15 syl9 
 |-  ( -. w = B -> ( ( ( w = x \/ w = x ) -> w e. z ) -> ( ( w = x \/ w = B ) -> w e. z ) ) )
17 16 al2imi 
 |-  ( A. w -. w = B -> ( A. w ( ( w = x \/ w = x ) -> w e. z ) -> A. w ( ( w = x \/ w = B ) -> w e. z ) ) )
18 13 17 sylbir 
 |-  ( -. E. w w = B -> ( A. w ( ( w = x \/ w = x ) -> w e. z ) -> A. w ( ( w = x \/ w = B ) -> w e. z ) ) )
19 18 eximdv 
 |-  ( -. E. w w = B -> ( E. z A. w ( ( w = x \/ w = x ) -> w e. z ) -> E. z A. w ( ( w = x \/ w = B ) -> w e. z ) ) )
20 12 19 mpi 
 |-  ( -. E. w w = B -> E. z A. w ( ( w = x \/ w = B ) -> w e. z ) )
21 11 20 pm2.61i 
 |-  E. z A. w ( ( w = x \/ w = B ) -> w e. z )
22 eqtr3 
 |-  ( ( w = A /\ x = A ) -> w = x )
23 22 expcom 
 |-  ( x = A -> ( w = A -> w = x ) )
24 23 orim1d 
 |-  ( x = A -> ( ( w = A \/ w = B ) -> ( w = x \/ w = B ) ) )
25 24 imim1d 
 |-  ( x = A -> ( ( ( w = x \/ w = B ) -> w e. z ) -> ( ( w = A \/ w = B ) -> w e. z ) ) )
26 25 alimdv 
 |-  ( x = A -> ( A. w ( ( w = x \/ w = B ) -> w e. z ) -> A. w ( ( w = A \/ w = B ) -> w e. z ) ) )
27 26 eximdv 
 |-  ( x = A -> ( E. z A. w ( ( w = x \/ w = B ) -> w e. z ) -> E. z A. w ( ( w = A \/ w = B ) -> w e. z ) ) )
28 21 27 mpi 
 |-  ( x = A -> E. z A. w ( ( w = A \/ w = B ) -> w e. z ) )