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 ⊢∃yx∈y∧∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v∧∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y

Proof

Step Hyp Ref Expression
1 axgroth4 ⊢∃yx∈y∧∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y
2 3anass ⊢x∈y∧∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y↔x∈y∧∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y
3 dfss2 ⊢w⊆z↔∀uu∈w→u∈z
4 elin ⊢w∈y∩v↔w∈y∧w∈v
5 3 4 imbi12i ⊢w⊆z→w∈y∩v↔∀uu∈w→u∈z→w∈y∧w∈v
6 5 albii ⊢∀ww⊆z→w∈y∩v↔∀w∀uu∈w→u∈z→w∈y∧w∈v
7 6 rexbii ⊢∃v∈y∀ww⊆z→w∈y∩v↔∃v∈y∀w∀uu∈w→u∈z→w∈y∧w∈v
8 df-rex ⊢∃v∈y∀w∀uu∈w→u∈z→w∈y∧w∈v↔∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v
9 7 8 bitri ⊢∃v∈y∀ww⊆z→w∈y∩v↔∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v
10 9 ralbii ⊢∀z∈y∃v∈y∀ww⊆z→w∈y∩v↔∀z∈y∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v
11 df-ral ⊢∀z∈y∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v↔∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v
12 10 11 bitri ⊢∀z∈y∃v∈y∀ww⊆z→w∈y∩v↔∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v
13 dfss2 ⊢z⊆y↔∀ww∈z→w∈y
14 vex ⊢y∈V
15 14 difexi ⊢y∖z∈V
16 vex ⊢z∈V
17 disjdifr ⊢y∖z∩z=∅
18 15 16 17 brdom6disj ⊢y∖z≼z↔∃w∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w
19 18 orbi1i ⊢y∖z≼z∨z∈y↔∃w∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y
20 19.44v ⊢∃w∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y↔∃w∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y
21 19 20 bitr4i ⊢y∖z≼z∨z∈y↔∃w∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y
22 13 21 imbi12i ⊢z⊆y→y∖z≼z∨z∈y↔∀ww∈z→w∈y→∃w∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y
23 19.35 ⊢∃ww∈z→w∈y→∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y↔∀ww∈z→w∈y→∃w∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y
24 22 23 bitr4i ⊢z⊆y→y∖z≼z∨z∈y↔∃ww∈z→w∈y→∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y
25 grothprimlem ⊢vu∈w↔∃gg∈w∧∀hh∈g↔h=v∨h=u
26 25 mobii ⊢∃*uvu∈w↔∃*u∃gg∈w∧∀hh∈g↔h=v∨h=u
27 df-mo ⊢∃*u∃gg∈w∧∀hh∈g↔h=v∨h=u↔∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t
28 26 27 bitri ⊢∃*uvu∈w↔∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t
29 28 ralbii ⊢∀v∈z∃*uvu∈w↔∀v∈z∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t
30 df-ral ⊢∀v∈z∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t↔∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t
31 29 30 bitri ⊢∀v∈z∃*uvu∈w↔∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t
32 df-ral ⊢∀v∈y∖z∃u∈zuv∈w↔∀vv∈y∖z→∃u∈zuv∈w
33 eldif ⊢v∈y∖z↔v∈y∧¬v∈z
34 grothprimlem ⊢uv∈w↔∃gg∈w∧∀hh∈g↔h=u∨h=v
35 34 rexbii ⊢∃u∈zuv∈w↔∃u∈z∃gg∈w∧∀hh∈g↔h=u∨h=v
36 df-rex ⊢∃u∈z∃gg∈w∧∀hh∈g↔h=u∨h=v↔∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v
37 35 36 bitri ⊢∃u∈zuv∈w↔∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v
38 33 37 imbi12i ⊢v∈y∖z→∃u∈zuv∈w↔v∈y∧¬v∈z→∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v
39 pm5.6 ⊢v∈y∧¬v∈z→∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v↔v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v
40 38 39 bitri ⊢v∈y∖z→∃u∈zuv∈w↔v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v
41 40 albii ⊢∀vv∈y∖z→∃u∈zuv∈w↔∀vv∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v
42 32 41 bitri ⊢∀v∈y∖z∃u∈zuv∈w↔∀vv∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v
43 31 42 anbi12i ⊢∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w↔∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧∀vv∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v
44 19.26 ⊢∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v↔∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧∀vv∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v
45 43 44 bitr4i ⊢∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w↔∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v
46 45 orbi1i ⊢∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y↔∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
47 46 imbi2i ⊢w∈z→w∈y→∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y↔w∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
48 47 exbii ⊢∃ww∈z→w∈y→∀v∈z∃*uvu∈w∧∀v∈y∖z∃u∈zuv∈w∨z∈y↔∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
49 24 48 bitri ⊢z⊆y→y∖z≼z∨z∈y↔∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
50 49 albii ⊢∀zz⊆y→y∖z≼z∨z∈y↔∀z∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
51 12 50 anbi12i ⊢∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y↔∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v∧∀z∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
52 19.26 ⊢∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v∧∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y↔∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v∧∀z∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
53 51 52 bitr4i ⊢∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y↔∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v∧∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
54 53 anbi2i ⊢x∈y∧∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y↔x∈y∧∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v∧∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
55 2 54 bitri ⊢x∈y∧∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y↔x∈y∧∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v∧∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
56 55 exbii ⊢∃yx∈y∧∀z∈y∃v∈y∀ww⊆z→w∈y∩v∧∀zz⊆y→y∖z≼z∨z∈y↔∃yx∈y∧∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v∧∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y
57 1 56 mpbi ⊢∃yx∈y∧∀zz∈y→∃vv∈y∧∀w∀uu∈w→u∈z→w∈y∧w∈v∧∃ww∈z→w∈y→∀vv∈z→∃t∀u∃gg∈w∧∀hh∈g↔h=v∨h=u→u=t∧v∈y→v∈z∨∃uu∈z∧∃gg∈w∧∀hh∈g↔h=u∨h=v∨z∈y