Definition df-gzrep 30605

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.)

Assertion

Ref	Expression
df-gzrep	⊢ AxRep = (𝑢 ∈ (Fmla‘ω) ↦ (∀𝑔3𝑜∃𝑔1𝑜∀𝑔2𝑜(∀𝑔1𝑜𝑢 →𝑔 (2𝑜=𝑔1𝑜)) →𝑔 ∀𝑔1𝑜∀𝑔2𝑜((2𝑜∈𝑔1𝑜) ↔𝑔 ∃𝑔3𝑜((3𝑜∈𝑔∅)∧𝑔∀𝑔1𝑜𝑢))))

Detailed syntax breakdown of Definition df-gzrep

Step	Hyp	Ref	Expression
1		cgzr 30598	. 2 class AxRep
2		vu	. . 3 setvar 𝑢
3		com 6957	. . . 4 class ω
4		cfmla 30573	. . . 4 class Fmla
5	3, 4	cfv 5804	. . 3 class (Fmla‘ω)
6	2	cv 1474	. . . . . . . . 9 class 𝑢
7		c1o 7440	. . . . . . . . 9 class 1𝑜
8	6, 7	cgol 30571	. . . . . . . 8 class ∀𝑔1𝑜𝑢
9		c2o 7441	. . . . . . . . 9 class 2𝑜
10		cgoq 30587	. . . . . . . . 9 class =𝑔
11	9, 7, 10	co 6549	. . . . . . . 8 class (2𝑜=𝑔1𝑜)
12		cgoi 30584	. . . . . . . 8 class →𝑔
13	8, 11, 12	co 6549	. . . . . . 7 class (∀𝑔1𝑜𝑢 →𝑔 (2𝑜=𝑔1𝑜))
14	13, 9	cgol 30571	. . . . . 6 class ∀𝑔2𝑜(∀𝑔1𝑜𝑢 →𝑔 (2𝑜=𝑔1𝑜))
15	14, 7	cgox 30588	. . . . 5 class ∃𝑔1𝑜∀𝑔2𝑜(∀𝑔1𝑜𝑢 →𝑔 (2𝑜=𝑔1𝑜))
16		c3o 7442	. . . . 5 class 3𝑜
17	15, 16	cgol 30571	. . . 4 class ∀𝑔3𝑜∃𝑔1𝑜∀𝑔2𝑜(∀𝑔1𝑜𝑢 →𝑔 (2𝑜=𝑔1𝑜))
18		cgoe 30569	. . . . . . . 8 class ∈𝑔
19	9, 7, 18	co 6549	. . . . . . 7 class (2𝑜∈𝑔1𝑜)
20		c0 3874	. . . . . . . . . 10 class ∅
21	16, 20, 18	co 6549	. . . . . . . . 9 class (3𝑜∈𝑔∅)
22		cgoa 30583	. . . . . . . . 9 class ∧𝑔
23	21, 8, 22	co 6549	. . . . . . . 8 class ((3𝑜∈𝑔∅)∧𝑔∀𝑔1𝑜𝑢)
24	23, 16	cgox 30588	. . . . . . 7 class ∃𝑔3𝑜((3𝑜∈𝑔∅)∧𝑔∀𝑔1𝑜𝑢)
25		cgob 30586	. . . . . . 7 class ↔𝑔
26	19, 24, 25	co 6549	. . . . . 6 class ((2𝑜∈𝑔1𝑜) ↔𝑔 ∃𝑔3𝑜((3𝑜∈𝑔∅)∧𝑔∀𝑔1𝑜𝑢))
27	26, 9	cgol 30571	. . . . 5 class ∀𝑔2𝑜((2𝑜∈𝑔1𝑜) ↔𝑔 ∃𝑔3𝑜((3𝑜∈𝑔∅)∧𝑔∀𝑔1𝑜𝑢))
28	27, 7	cgol 30571	. . . 4 class ∀𝑔1𝑜∀𝑔2𝑜((2𝑜∈𝑔1𝑜) ↔𝑔 ∃𝑔3𝑜((3𝑜∈𝑔∅)∧𝑔∀𝑔1𝑜𝑢))
29	17, 28, 12	co 6549	. . 3 class (∀𝑔3𝑜∃𝑔1𝑜∀𝑔2𝑜(∀𝑔1𝑜𝑢 →𝑔 (2𝑜=𝑔1𝑜)) →𝑔 ∀𝑔1𝑜∀𝑔2𝑜((2𝑜∈𝑔1𝑜) ↔𝑔 ∃𝑔3𝑜((3𝑜∈𝑔∅)∧𝑔∀𝑔1𝑜𝑢)))
30	2, 5, 29	cmpt 4643	. 2 class (𝑢 ∈ (Fmla‘ω) ↦ (∀𝑔3𝑜∃𝑔1𝑜∀𝑔2𝑜(∀𝑔1𝑜𝑢 →𝑔 (2𝑜=𝑔1𝑜)) →𝑔 ∀𝑔1𝑜∀𝑔2𝑜((2𝑜∈𝑔1𝑜) ↔𝑔 ∃𝑔3𝑜((3𝑜∈𝑔∅)∧𝑔∀𝑔1𝑜𝑢))))
31	1, 30	wceq 1475	1 wff AxRep = (𝑢 ∈ (Fmla‘ω) ↦ (∀𝑔3𝑜∃𝑔1𝑜∀𝑔2𝑜(∀𝑔1𝑜𝑢 →𝑔 (2𝑜=𝑔1𝑜)) →𝑔 ∀𝑔1𝑜∀𝑔2𝑜((2𝑜∈𝑔1𝑜) ↔𝑔 ∃𝑔3𝑜((3𝑜∈𝑔∅)∧𝑔∀𝑔1𝑜𝑢))))

This definition is referenced by: (None)