Metamath Proof Explorer

Definition df-gzinf

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

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

Detailed syntax breakdown

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