Metamath Proof Explorer

Theorem grothprim

Description: The Tarski-Grothendieck Axiom ax-groth expanded into set theory primitives using 163 symbols (allowing the defined symbols /\ , \/ , <-> , and E. ). An open problem is whether a shorter equivalent exists (when expanded to primitives). (Contributed by NM, 16-Apr-2007)

Ref Expression
Assertion grothprim 
|- E. y ( x e. y /\ A. z ( ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) /\ E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) ) )

Proof

Step Hyp Ref Expression
1 axgroth4 
 |-  E. y ( x e. y /\ A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) /\ A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) )
2 3anass 
 |-  ( ( x e. y /\ A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) /\ A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) ) <-> ( x e. y /\ ( A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) /\ A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) ) ) )
3 dfss2 
 |-  ( w C_ z <-> A. u ( u e. w -> u e. z ) )
4 elin 
 |-  ( w e. ( y i^i v ) <-> ( w e. y /\ w e. v ) )
5 3 4 imbi12i 
 |-  ( ( w C_ z -> w e. ( y i^i v ) ) <-> ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) )
6 5 albii 
 |-  ( A. w ( w C_ z -> w e. ( y i^i v ) ) <-> A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) )
7 6 rexbii 
 |-  ( E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) <-> E. v e. y A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) )
8 df-rex 
 |-  ( E. v e. y A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) <-> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) )
9 7 8 bitri 
 |-  ( E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) <-> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) )
10 9 ralbii 
 |-  ( A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) <-> A. z e. y E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) )
11 df-ral 
 |-  ( A. z e. y E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) <-> A. z ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) )
12 10 11 bitri 
 |-  ( A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) <-> A. z ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) )
13 dfss2 
 |-  ( z C_ y <-> A. w ( w e. z -> w e. y ) )
14 vex 
 |-  y e. _V
15 14 difexi 
 |-  ( y \ z ) e. _V
16 vex 
 |-  z e. _V
17 incom 
 |-  ( ( y \ z ) i^i z ) = ( z i^i ( y \ z ) )
18 disjdif 
 |-  ( z i^i ( y \ z ) ) = (/)
19 17 18 eqtri 
 |-  ( ( y \ z ) i^i z ) = (/)
20 15 16 19 brdom6disj 
 |-  ( ( y \ z ) ~<_ z <-> E. w ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) )
21 20 orbi1i 
 |-  ( ( ( y \ z ) ~<_ z \/ z e. y ) <-> ( E. w ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) )
22 19.44v 
 |-  ( E. w ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) <-> ( E. w ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) )
23 21 22 bitr4i 
 |-  ( ( ( y \ z ) ~<_ z \/ z e. y ) <-> E. w ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) )
24 13 23 imbi12i 
 |-  ( ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) <-> ( A. w ( w e. z -> w e. y ) -> E. w ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) ) )
25 19.35 
 |-  ( E. w ( ( w e. z -> w e. y ) -> ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) ) <-> ( A. w ( w e. z -> w e. y ) -> E. w ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) ) )
26 24 25 bitr4i 
 |-  ( ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) <-> E. w ( ( w e. z -> w e. y ) -> ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) ) )
27 grothprimlem 
 |-  ( { v , u } e. w <-> E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) )
28 27 mobii 
 |-  ( E* u { v , u } e. w <-> E* u E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) )
29 df-mo 
 |-  ( E* u E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) <-> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) )
30 28 29 bitri 
 |-  ( E* u { v , u } e. w <-> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) )
31 30 ralbii 
 |-  ( A. v e. z E* u { v , u } e. w <-> A. v e. z E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) )
32 df-ral 
 |-  ( A. v e. z E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) <-> A. v ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) )
33 31 32 bitri 
 |-  ( A. v e. z E* u { v , u } e. w <-> A. v ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) )
34 df-ral 
 |-  ( A. v e. ( y \ z ) E. u e. z { u , v } e. w <-> A. v ( v e. ( y \ z ) -> E. u e. z { u , v } e. w ) )
35 eldif 
 |-  ( v e. ( y \ z ) <-> ( v e. y /\ -. v e. z ) )
36 grothprimlem 
 |-  ( { u , v } e. w <-> E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) )
37 36 rexbii 
 |-  ( E. u e. z { u , v } e. w <-> E. u e. z E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) )
38 df-rex 
 |-  ( E. u e. z E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) <-> E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) )
39 37 38 bitri 
 |-  ( E. u e. z { u , v } e. w <-> E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) )
40 35 39 imbi12i 
 |-  ( ( v e. ( y \ z ) -> E. u e. z { u , v } e. w ) <-> ( ( v e. y /\ -. v e. z ) -> E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) )
41 pm5.6 
 |-  ( ( ( v e. y /\ -. v e. z ) -> E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) <-> ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) )
42 40 41 bitri 
 |-  ( ( v e. ( y \ z ) -> E. u e. z { u , v } e. w ) <-> ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) )
43 42 albii 
 |-  ( A. v ( v e. ( y \ z ) -> E. u e. z { u , v } e. w ) <-> A. v ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) )
44 34 43 bitri 
 |-  ( A. v e. ( y \ z ) E. u e. z { u , v } e. w <-> A. v ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) )
45 33 44 anbi12i 
 |-  ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) <-> ( A. v ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ A. v ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) )
46 19.26 
 |-  ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) <-> ( A. v ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ A. v ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) )
47 45 46 bitr4i 
 |-  ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) <-> A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) )
48 47 orbi1i 
 |-  ( ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) <-> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) )
49 48 imbi2i 
 |-  ( ( ( w e. z -> w e. y ) -> ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) ) <-> ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) )
50 49 exbii 
 |-  ( E. w ( ( w e. z -> w e. y ) -> ( ( A. v e. z E* u { v , u } e. w /\ A. v e. ( y \ z ) E. u e. z { u , v } e. w ) \/ z e. y ) ) <-> E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) )
51 26 50 bitri 
 |-  ( ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) <-> E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) )
52 51 albii 
 |-  ( A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) <-> A. z E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) )
53 12 52 anbi12i 
 |-  ( ( A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) /\ A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) ) <-> ( A. z ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) /\ A. z E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) ) )
54 19.26 
 |-  ( A. z ( ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) /\ E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) ) <-> ( A. z ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) /\ A. z E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) ) )
55 53 54 bitr4i 
 |-  ( ( A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) /\ A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) ) <-> A. z ( ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) /\ E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) ) )
56 55 anbi2i 
 |-  ( ( x e. y /\ ( A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) /\ A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) ) ) <-> ( x e. y /\ A. z ( ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) /\ E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) ) ) )
57 2 56 bitri 
 |-  ( ( x e. y /\ A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) /\ A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) ) <-> ( x e. y /\ A. z ( ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) /\ E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) ) ) )
58 57 exbii 
 |-  ( E. y ( x e. y /\ A. z e. y E. v e. y A. w ( w C_ z -> w e. ( y i^i v ) ) /\ A. z ( z C_ y -> ( ( y \ z ) ~<_ z \/ z e. y ) ) ) <-> E. y ( x e. y /\ A. z ( ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) /\ E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) ) ) )
59 1 58 mpbi 
 |-  E. y ( x e. y /\ A. z ( ( z e. y -> E. v ( v e. y /\ A. w ( A. u ( u e. w -> u e. z ) -> ( w e. y /\ w e. v ) ) ) ) /\ E. w ( ( w e. z -> w e. y ) -> ( A. v ( ( v e. z -> E. t A. u ( E. g ( g e. w /\ A. h ( h e. g <-> ( h = v \/ h = u ) ) ) -> u = t ) ) /\ ( v e. y -> ( v e. z \/ E. u ( u e. z /\ E. g ( g e. w /\ A. h ( h e. g <-> ( h = u \/ h = v ) ) ) ) ) ) ) \/ z e. y ) ) ) )