df-gzrep

Description: The Godel-set version of the Axiom Scheme of Replacement. Since this is a scheme and not a single axiom, it manifests as a function on wffs, each giving rise to a different axiom. (Contributed by Mario Carneiro, 14-Jul-2013)

		Ref	Expression
	Assertion	df-gzrep	$⊢ AxRep = (u \in Fmla (ω) ⟼ [\forall_{𝑔} 3_{𝑜} [\exists_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} u] \to_{𝑔} (2_{𝑜} =_{𝑔} 1_{𝑜}))]]] \to_{𝑔} [\forall_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \leftrightarrow_{𝑔} [\exists_{𝑔} 3_{𝑜} ((3_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 1_{𝑜} u])])]])$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgzr	$class AxRep$
1		vu	$setvar u$
2		cfmla	$class Fmla$
3		com	$class ω$
4	3 2	cfv	$class Fmla (ω)$
5		c3o	$class 3_{𝑜}$
6		c1o	$class 1_{𝑜}$
7		c2o	$class 2_{𝑜}$
8	1	cv	$setvar u$
9	8 6	cgol	$class [\forall_{𝑔} 1_{𝑜} u]$
10		cgoi	$class \to_{𝑔}$
11		cgoq	$class =_{𝑔}$
12	7 6 11	co	$class (2_{𝑜} =_{𝑔} 1_{𝑜})$
13	9 12 10	co	$class ([\forall_{𝑔} 1_{𝑜} u] \to_{𝑔} (2_{𝑜} =_{𝑔} 1_{𝑜}))$
14	13 7	cgol	$class [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} u] \to_{𝑔} (2_{𝑜} =_{𝑔} 1_{𝑜}))]$
15	14 6	cgox	$class [\exists_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} u] \to_{𝑔} (2_{𝑜} =_{𝑔} 1_{𝑜}))]]$
16	15 5	cgol	$class [\forall_{𝑔} 3_{𝑜} [\exists_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} u] \to_{𝑔} (2_{𝑜} =_{𝑔} 1_{𝑜}))]]]$
17		cgoe	$class \in_{𝑔}$
18	7 6 17	co	$class (2_{𝑜} \in_{𝑔} 1_{𝑜})$
19		cgob	$class \leftrightarrow_{𝑔}$
20		c0	$class \emptyset$
21	5 20 17	co	$class (3_{𝑜} \in_{𝑔} \emptyset)$
22		cgoa	$class \land_{𝑔}$
23	21 9 22	co	$class ((3_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 1_{𝑜} u])$
24	23 5	cgox	$class [\exists_{𝑔} 3_{𝑜} ((3_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 1_{𝑜} u])]$
25	18 24 19	co	$class ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \leftrightarrow_{𝑔} [\exists_{𝑔} 3_{𝑜} ((3_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 1_{𝑜} u])])$
26	25 7	cgol	$class [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \leftrightarrow_{𝑔} [\exists_{𝑔} 3_{𝑜} ((3_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 1_{𝑜} u])])]$
27	26 6	cgol	$class [\forall_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \leftrightarrow_{𝑔} [\exists_{𝑔} 3_{𝑜} ((3_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 1_{𝑜} u])])]]$
28	16 27 10	co	$class ([\forall_{𝑔} 3_{𝑜} [\exists_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} u] \to_{𝑔} (2_{𝑜} =_{𝑔} 1_{𝑜}))]]] \to_{𝑔} [\forall_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \leftrightarrow_{𝑔} [\exists_{𝑔} 3_{𝑜} ((3_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 1_{𝑜} u])])]])$
29	1 4 28	cmpt	$class (u \in Fmla (ω) ⟼ [\forall_{𝑔} 3_{𝑜} [\exists_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} u] \to_{𝑔} (2_{𝑜} =_{𝑔} 1_{𝑜}))]]] \to_{𝑔} [\forall_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \leftrightarrow_{𝑔} [\exists_{𝑔} 3_{𝑜} ((3_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 1_{𝑜} u])])]])$
30	0 29	wceq	$wff AxRep = (u \in Fmla (ω) ⟼ [\forall_{𝑔} 3_{𝑜} [\exists_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ([\forall_{𝑔} 1_{𝑜} u] \to_{𝑔} (2_{𝑜} =_{𝑔} 1_{𝑜}))]]] \to_{𝑔} [\forall_{𝑔} 1_{𝑜} [\forall_{𝑔} 2_{𝑜} ((2_{𝑜} \in_{𝑔} 1_{𝑜}) \leftrightarrow_{𝑔} [\exists_{𝑔} 3_{𝑜} ((3_{𝑜} \in_{𝑔} \emptyset) \land_{𝑔} [\forall_{𝑔} 1_{𝑜} u])])]])$

Metamath Proof Explorer

Definition df-gzrep

Detailed syntax breakdown