Theorem grothprim 8902

Description: Grothendieck's Axiom ax-groth 8896 expanded into set theory primitives using 163 symbols. An open problem is whether a shorter equivalent exists (when expanded to primitives).

Assertion

Ref	Expression
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.tA.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))))

Distinct variable group:   x,y,z,w,v,u,t,h,g

Proof of Theorem grothprim

Step	Hyp	Ref	Expression
1		axgroth4 8899	. 2 |- E.y(x e. y /\ A.z e. y E.v e. y A.w(w (_ z -> w e. (y i^i v)) /\ A.z(z (_ y -> ((y \ z) ~<_ z \/ z e. y)))
2		3anass 782	. . . 4 |- ((x e. y /\ A.z e. y E.v e. y A.w(w (_ z -> w e. (y i^i v)) /\ A.z(z (_ y -> ((y \ z) ~<_ z \/ z e. y))) <-> (x e. y /\ (A.z e. y E.v e. y A.w(w (_ z -> w e. (y i^i v)) /\ A.z(z (_ y -> ((y \ z) ~<_ z \/ z e. y)))))
3		dfss2 2102	. . . . . . . . . . . . 13 |- (w (_ z <-> A.u(u e. w -> u e. z))
4		elin 2251	. . . . . . . . . . . . 13 |- (w e. (y i^i v) <-> (w e. y /\ w e. v))
5	3, 4	imbi12i 186	. . . . . . . . . . . 12 |- ((w (_ z -> w e. (y i^i v)) <-> (A.u(u e. w -> u e. z) -> (w e. y /\ w e. v)))
6	5	albii 1031	. . . . . . . . . . 11 |- (A.w(w (_ 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 1706	. . . . . . . . . 10 |- (E.v e. y A.w(w (_ 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 1688	. . . . . . . . . 10 |- (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 171	. . . . . . . . 9 |- (E.v e. y A.w(w (_ 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 1705	. . . . . . . 8 |- (A.z e. y E.v e. y A.w(w (_ 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 1687	. . . . . . . 8 |- (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 171	. . . . . . 7 |- (A.z e. y E.v e. y A.w(w (_ 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 2102	. . . . . . . . . 10 |- (z (_ y <-> A.w(w e. z -> w e. y))
14		visset 1851	. . . . . . . . . . . . . 14 |- y e. V
15		difexg 2773	. . . . . . . . . . . . . 14 |- (y e. V -> (y \ z) e. V)
16	14, 15	ax-mp 7	. . . . . . . . . . . . 13 |- (y \ z) e. V
17		visset 1851	. . . . . . . . . . . . 13 |- z e. V
18		incom 2252	. . . . . . . . . . . . . 14 |- ((y \ z) i^i z) = (z i^i (y \ z))
19		difdisj 2382	. . . . . . . . . . . . . 14 |- (z i^i (y \ z)) = (/)
20	18, 19	eqtri 1532	. . . . . . . . . . . . 13 |- ((y \ z) i^i z) = (/)
21	16, 17, 20	brdom6disj 4891	. . . . . . . . . . . 12 |- ((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))
22	21	orbi1i 254	. . . . . . . . . . 11 |- (((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))
23		ax-17 1003	. . . . . . . . . . . 12 |- (z e. y -> A.w z e. y)
24	23	19.44 1121	. . . . . . . . . . 11 |- (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))
25	22, 24	bitr4i 174	. . . . . . . . . 10 |- (((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))
26	13, 25	imbi12i 186	. . . . . . . . 9 |- ((z (_ 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)))
27		19.35 1107	. . . . . . . . 9 |- (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)))
28		grothprimlem 8901	. . . . . . . . . . . . . . . . . 18 |- ({v, u} e. w <-> E.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))))
29	28	mobii 1438	. . . . . . . . . . . . . . . . 17 |- (E*u{v, u} e. w <-> E*uE.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))))
30		ax-17 1003	. . . . . . . . . . . . . . . . . 18 |- (E.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))) -> A.tE.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))))
31	30	mo2 1433	. . . . . . . . . . . . . . . . 17 |- (E*uE.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))) <-> E.tA.u(E.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))) -> u = t))
32	29, 31	bitri 171	. . . . . . . . . . . . . . . 16 |- (E*u{v, u} e. w <-> E.tA.u(E.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))) -> u = t))
33	32	ralbii 1705	. . . . . . . . . . . . . . 15 |- (A.v e. z E*u{v, u} e. w <-> A.v e. z E.tA.u(E.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))) -> u = t))
34		df-ral 1687	. . . . . . . . . . . . . . 15 |- (A.v e. z E.tA.u(E.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))) -> u = t) <-> A.v(v e. z -> E.tA.u(E.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))) -> u = t)))
35	33, 34	bitri 171	. . . . . . . . . . . . . 14 |- (A.v e. z E*u{v, u} e. w <-> A.v(v e. z -> E.tA.u(E.g(g e. w /\ A.h(h e. g <-> (h = v \/ h = u))) -> u = t)))
36		df-ral 1687	. . . . . . . . . . . . . . 15 |- (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))
37		impexp 345	. . . . . . . . . . . . . . . . 17 |- (((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)))))))
38		eldif 2101	. . . . . . . . . . . . . . . . . 18 |- (v e. (y \ z) <-> (v e. y /\ -. v e. z))
39		grothprimlem 8901	. . . . . . . . . . . . . . . . . . . 20 |- ({u, v} e. w <-> E.g(g e. w /\ A.h(h e. g <-> (h = u \/ h = v))))
40	39	rexbii 1706	. . . . . . . . . . . . . . . . . . 19 |- (E.u e. z {u, v} e. w <-> E.u e. z E.