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 df-ss ⊢ 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 df-ss ⊢ z ⊆ y ↔ ∀ w w ∈ 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 ∃* u v u ∈ w ∧ ∀ v ∈ y ∖ z ∃ u ∈ z u v ∈ w
19 18 orbi1i ⊢ y ∖ z ≼ z ∨ z ∈ y ↔ ∃ w ∀ v ∈ z ∃* u v u ∈ w ∧ ∀ v ∈ y ∖ z ∃ u ∈ z u v ∈ w ∨ z ∈ y
20 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
21 19 20 bitr4i ⊢ y ∖ z ≼ z ∨ z ∈ y ↔ ∃ w ∀ v ∈ z ∃* u v u ∈ w ∧ ∀ v ∈ y ∖ z ∃ u ∈ z u v ∈ w ∨ z ∈ y
22 13 21 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
23 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
24 22 23 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
25 grothprimlem ⊢ v u ∈ w ↔ ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = v ∨ h = u
26 25 mobii ⊢ ∃* u v u ∈ w ↔ ∃* u ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = v ∨ h = u
27 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
28 26 27 bitri ⊢ ∃* u v u ∈ w ↔ ∃ t ∀ u ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = v ∨ h = u → u = t
29 28 ralbii ⊢ ∀ v ∈ z ∃* u v u ∈ w ↔ ∀ v ∈ z ∃ t ∀ u ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = v ∨ h = u → u = t
30 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
31 29 30 bitri ⊢ ∀ v ∈ z ∃* u v u ∈ w ↔ ∀ v v ∈ z → ∃ t ∀ u ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = v ∨ h = u → u = t
32 df-ral ⊢ ∀ v ∈ y ∖ z ∃ u ∈ z u v ∈ w ↔ ∀ v v ∈ y ∖ z → ∃ u ∈ z u v ∈ w
33 eldif ⊢ v ∈ y ∖ z ↔ v ∈ y ∧ ¬ v ∈ z
34 grothprimlem ⊢ u v ∈ w ↔ ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = u ∨ h = v
35 34 rexbii ⊢ ∃ u ∈ z u v ∈ w ↔ ∃ u ∈ z ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = u ∨ h = v
36 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
37 35 36 bitri ⊢ ∃ u ∈ z u v ∈ w ↔ ∃ u u ∈ z ∧ ∃ g g ∈ w ∧ ∀ h h ∈ g ↔ h = u ∨ h = v
38 33 37 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
39 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
40 38 39 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
41 40 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
42 32 41 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
43 31 42 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
44 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
45 43 44 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
46 45 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
47 46 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
48 47 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
49 24 48 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
50 49 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
51 12 50 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
52 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
53 51 52 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
54 53 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
55 2 54 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
56 55 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
57 1 56 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