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 ⊢ ∃ y x ∈ y ∧ ∀ z z ∈ y → ∃ v v ∈ y ∧ ∀ w ∀ u u ∈ w → u ∈ z → w ∈ y ∧ w ∈ v ∧ ∃ w w ∈ z → w ∈ y → ∀ v v ∈ z → ∃ t ∀ u ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = v ∨ h = u → u = t ∧ v ∈ y → v ∈ z ∨ ∃ u u ∈ z ∧ ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = u ∨ h = v ∨ z ∈ y

Proof

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