Metamath Proof Explorer

Theorem axgroth2

Description: Alternate version of the Tarski-Grothendieck Axiom. (Contributed by NM, 18-Mar-2007)

Ref Expression
Assertion axgroth2 
|- E. y ( x e. y /\ A. z e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) /\ A. z ( z C_ y -> ( y ~<_ z \/ z e. y ) ) )

Proof

Step Hyp Ref Expression
1 ax-groth 
 |-  E. y ( x e. y /\ A. z e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) /\ A. z ( z C_ y -> ( z ~~ y \/ z e. y ) ) )
2 ssdomg 
 |-  ( y e. _V -> ( z C_ y -> z ~<_ y ) )
3 2 elv 
 |-  ( z C_ y -> z ~<_ y )
4 3 biantrurd 
 |-  ( z C_ y -> ( y ~<_ z <-> ( z ~<_ y /\ y ~<_ z ) ) )
5 sbthb 
 |-  ( ( z ~<_ y /\ y ~<_ z ) <-> z ~~ y )
6 4 5 bitrdi 
 |-  ( z C_ y -> ( y ~<_ z <-> z ~~ y ) )
7 6 orbi1d 
 |-  ( z C_ y -> ( ( y ~<_ z \/ z e. y ) <-> ( z ~~ y \/ z e. y ) ) )
8 7 pm5.74i 
 |-  ( ( z C_ y -> ( y ~<_ z \/ z e. y ) ) <-> ( z C_ y -> ( z ~~ y \/ z e. y ) ) )
9 8 albii 
 |-  ( A. z ( z C_ y -> ( y ~<_ z \/ z e. y ) ) <-> A. z ( z C_ y -> ( z ~~ y \/ z e. y ) ) )
10 9 3anbi3i 
 |-  ( ( x e. y /\ A. z e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) /\ A. z ( z C_ y -> ( y ~<_ z \/ z e. y ) ) ) <-> ( x e. y /\ A. z e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) /\ A. z ( z C_ y -> ( z ~~ y \/ z e. y ) ) ) )
11 10 exbii 
 |-  ( E. y ( x e. y /\ A. z e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) /\ A. z ( z C_ y -> ( y ~<_ z \/ z e. y ) ) ) <-> E. y ( x e. y /\ A. z e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) /\ A. z ( z C_ y -> ( z ~~ y \/ z e. y ) ) ) )
12 1 11 mpbir 
 |-  E. y ( x e. y /\ A. z e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) /\ A. z ( z C_ y -> ( y ~<_ z \/ z e. y ) ) )