Metamath Proof Explorer

Theorem grothtsk

Description: The Tarski-Grothendieck Axiom, using abbreviations. (Contributed by Mario Carneiro, 28-May-2013)

Ref Expression
Assertion grothtsk 
|- U. Tarski = _V

Proof

Step Hyp Ref Expression
1 axgroth5 
 |-  E. x ( w e. x /\ A. y e. x ( ~P y C_ x /\ E. z e. x ~P y C_ z ) /\ A. y e. ~P x ( y ~~ x \/ y e. x ) )
2 eltskg 
 |-  ( x e. _V -> ( x e. Tarski <-> ( A. y e. x ( ~P y C_ x /\ E. z e. x ~P y C_ z ) /\ A. y e. ~P x ( y ~~ x \/ y e. x ) ) ) )
3 2 elv 
 |-  ( x e. Tarski <-> ( A. y e. x ( ~P y C_ x /\ E. z e. x ~P y C_ z ) /\ A. y e. ~P x ( y ~~ x \/ y e. x ) ) )
4 3 anbi2i 
 |-  ( ( w e. x /\ x e. Tarski ) <-> ( w e. x /\ ( A. y e. x ( ~P y C_ x /\ E. z e. x ~P y C_ z ) /\ A. y e. ~P x ( y ~~ x \/ y e. x ) ) ) )
5 3anass 
 |-  ( ( w e. x /\ A. y e. x ( ~P y C_ x /\ E. z e. x ~P y C_ z ) /\ A. y e. ~P x ( y ~~ x \/ y e. x ) ) <-> ( w e. x /\ ( A. y e. x ( ~P y C_ x /\ E. z e. x ~P y C_ z ) /\ A. y e. ~P x ( y ~~ x \/ y e. x ) ) ) )
6 4 5 bitr4i 
 |-  ( ( w e. x /\ x e. Tarski ) <-> ( w e. x /\ A. y e. x ( ~P y C_ x /\ E. z e. x ~P y C_ z ) /\ A. y e. ~P x ( y ~~ x \/ y e. x ) ) )
7 6 exbii 
 |-  ( E. x ( w e. x /\ x e. Tarski ) <-> E. x ( w e. x /\ A. y e. x ( ~P y C_ x /\ E. z e. x ~P y C_ z ) /\ A. y e. ~P x ( y ~~ x \/ y e. x ) ) )
8 1 7 mpbir 
 |-  E. x ( w e. x /\ x e. Tarski )
9 eluni 
 |-  ( w e. U. Tarski <-> E. x ( w e. x /\ x e. Tarski ) )
10 8 9 mpbir 
 |-  w e. U. Tarski
11 vex 
 |-  w e. _V
12 10 11 2th 
 |-  ( w e. U. Tarski <-> w e. _V )
13 12 eqriv 
 |-  U. Tarski = _V