Metamath Proof Explorer

Theorem axgroth3

Description: Alternate version of the Tarski-Grothendieck Axiom. ax-cc is used to derive this version. (Contributed by NM, 26-Mar-2007)

Ref Expression
Assertion axgroth3 
|- 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 \/ z e. y ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 ssid 
 |-  z C_ z
3 sseq1 
 |-  ( v = z -> ( v C_ z <-> z C_ z ) )
4 elequ1 
 |-  ( v = z -> ( v e. w <-> z e. w ) )
5 3 4 imbi12d 
 |-  ( v = z -> ( ( v C_ z -> v e. w ) <-> ( z C_ z -> z e. w ) ) )
6 5 spvv 
 |-  ( A. v ( v C_ z -> v e. w ) -> ( z C_ z -> z e. w ) )
7 2 6 mpi 
 |-  ( A. v ( v C_ z -> v e. w ) -> z e. w )
8 7 reximi 
 |-  ( E. w e. y A. v ( v C_ z -> v e. w ) -> E. w e. y z e. w )
9 eluni2 
 |-  ( z e. U. y <-> E. w e. y z e. w )
10 8 9 sylibr 
 |-  ( E. w e. y A. v ( v C_ z -> v e. w ) -> z e. U. y )
11 10 adantl 
 |-  ( ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) -> z e. U. y )
12 11 ralimi 
 |-  ( 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 e. y z e. U. y )
13 dfss3 
 |-  ( y C_ U. y <-> A. z e. y z e. U. y )
14 12 13 sylibr 
 |-  ( A. z e. y ( A. w ( w C_ z -> w e. y ) /\ E. w e. y A. v ( v C_ z -> v e. w ) ) -> y C_ U. y )
15 vex 
 |-  y e. _V
16 grothac 
 |-  dom card = _V
17 15 16 eleqtrri 
 |-  y e. dom card
18 vex 
 |-  z e. _V
19 18 16 eleqtrri 
 |-  z e. dom card
20 ne0i 
 |-  ( x e. y -> y =/= (/) )
21 15 dominf 
 |-  ( ( y =/= (/) /\ y C_ U. y ) -> _om ~<_ y )
22 20 21 sylan 
 |-  ( ( x e. y /\ y C_ U. y ) -> _om ~<_ y )
23 infdif2 
 |-  ( ( y e. dom card /\ z e. dom card /\ _om ~<_ y ) -> ( ( y \ z ) ~<_ z <-> y ~<_ z ) )
24 17 19 22 23 mp3an12i 
 |-  ( ( x e. y /\ y C_ U. y ) -> ( ( y \ z ) ~<_ z <-> y ~<_ z ) )
25 24 orbi1d 
 |-  ( ( x e. y /\ y C_ U. y ) -> ( ( ( y \ z ) ~<_ z \/ z e. y ) <-> ( y ~<_ z \/ z e. y ) ) )
26 25 imbi2d 
 |-  ( ( x e. y /\ y C_ U. y ) -> ( ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) <-> ( z C_ y -> ( y ~<_ z \/ z e. y ) ) ) )
27 26 albidv 
 |-  ( ( x e. y /\ y C_ U. y ) -> ( A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) <-> A. z ( z C_ y -> ( y ~<_ z \/ z e. y ) ) ) )
28 14 27 sylan2 
 |-  ( ( 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 \/ z e. y ) ) <-> A. z ( z C_ y -> ( y ~<_ z \/ z e. y ) ) ) )
29 28 pm5.32i 
 |-  ( ( ( 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 \/ 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 -> ( y ~<_ z \/ z e. y ) ) ) )
30 df-3an 
 |-  ( ( 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 \/ 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 -> ( ( y \ z ) ~<_ z \/ z e. y ) ) ) )
31 df-3an 
 |-  ( ( 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 -> ( y ~<_ z \/ z e. y ) ) ) )
32 29 30 31 3bitr4i 
 |-  ( ( 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 \/ 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 -> ( y ~<_ z \/ z e. y ) ) ) )
33 32 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 \/ 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 -> ( y ~<_ z \/ z e. y ) ) ) )
34 1 33 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 \/ z e. y ) ) )