Metamath Proof Explorer

Definition df-gzreg

Description: The Godel-set version of the Axiom of Regularity. (Contributed by Mario Carneiro, 14-Jul-2013)

		Ref	Expression
	Assertion	df-gzreg	$⊢ AxReg = [\exists_{𝑔} 1_{𝑜} (1_{𝑜} \in_{𝑔} \emptyset)] \to_{𝑔} [\exists_{𝑔} 1_{𝑜} ((1_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \to_{𝑔} [\neg_{𝑔} (2_{𝑜} \in_{𝑔} \emptyset)])])]$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgzg	$class AxReg$
1		c1o	$class 1_{𝑜}$
2		cgoe	$class \in_{𝑔}$
3		c0	$class \emptyset$
4	1 3 2	co	$class (1_{𝑜} \in_{𝑔} \emptyset)$
5	4 1	cgox	$class [\exists_{𝑔} 1_{𝑜} (1_{𝑜} \in_{𝑔} \emptyset)]$
6		cgoi	$class \to_{𝑔}$
7		cgoa	$class \land_{𝑔}$
8		c2o	$class 2_{𝑜}$
9	8 1 2	co	$class (2_{𝑜} \in_{𝑔} 1_{𝑜})$
10	8 3 2	co	$class (2_{𝑜} \in_{𝑔} \emptyset)$
11	10	cgon	$class [\neg_{𝑔} (2_{𝑜} \in_{𝑔} \emptyset)]$
12	9 11 6	co	$class ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \to_{𝑔} [\neg_{𝑔} (2_{𝑜} \in_{𝑔} \emptyset)])$
13	12 8	cgol	$class [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \to_{𝑔} [\neg_{𝑔} (2_{𝑜} \in_{𝑔} \emptyset)])]$
14	4 13 7	co	$class ((1_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \to_{𝑔} [\neg_{𝑔} (2_{𝑜} \in_{𝑔} \emptyset)])])$
15	14 1	cgox	$class [\exists_{𝑔} 1_{𝑜} ((1_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \to_{𝑔} [\neg_{𝑔} (2_{𝑜} \in_{𝑔} \emptyset)])])]$
16	5 15 6	co	$class ([\exists_{𝑔} 1_{𝑜} (1_{𝑜} \in_{𝑔} \emptyset)] \to_{𝑔} [\exists_{𝑔} 1_{𝑜} ((1_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \to_{𝑔} [\neg_{𝑔} (2_{𝑜} \in_{𝑔} \emptyset)])])])$
17	0 16	wceq	$wff AxReg = [\exists_{𝑔} 1_{𝑜} (1_{𝑜} \in_{𝑔} \emptyset)] \to_{𝑔} [\exists_{𝑔} 1_{𝑜} ((1_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \to_{𝑔} [\neg_{𝑔} (2_{𝑜} \in_{𝑔} \emptyset)])])]$