Definition df-gzrep 33316

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‘ω) ↦ (∀𝑔3o∃𝑔1o∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o)) →𝑔 ∀𝑔1o∀𝑔2o((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢))))

Detailed syntax breakdown of Definition df-gzrep

Step	Hyp	Ref	Expression
1		cgzr 33309	. 2 class AxRep
2		vu	. . 3 setvar 𝑢
3		com 7687	. . . 4 class ω
4		cfmla 33199	. . . 4 class Fmla
5	3, 4	cfv 6418	. . 3 class (Fmla‘ω)
6	2	cv 1538	. . . . . . . . 9 class 𝑢
7		c1o 8260	. . . . . . . . 9 class 1o
8	6, 7	cgol 33197	. . . . . . . 8 class ∀𝑔1o𝑢
9		c2o 8261	. . . . . . . . 9 class 2o
10		cgoq 33299	. . . . . . . . 9 class =𝑔
11	9, 7, 10	co 7255	. . . . . . . 8 class (2o=𝑔1o)
12		cgoi 33296	. . . . . . . 8 class →𝑔
13	8, 11, 12	co 7255	. . . . . . 7 class (∀𝑔1o𝑢 →𝑔 (2o=𝑔1o))
14	13, 9	cgol 33197	. . . . . 6 class ∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o))
15	14, 7	cgox 33300	. . . . 5 class ∃𝑔1o∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o))
16		c3o 8262	. . . . 5 class 3o
17	15, 16	cgol 33197	. . . 4 class ∀𝑔3o∃𝑔1o∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o))
18		cgoe 33195	. . . . . . . 8 class ∈𝑔
19	9, 7, 18	co 7255	. . . . . . 7 class (2o∈𝑔1o)
20		c0 4253	. . . . . . . . . 10 class ∅
21	16, 20, 18	co 7255	. . . . . . . . 9 class (3o∈𝑔∅)
22		cgoa 33295	. . . . . . . . 9 class ∧𝑔
23	21, 8, 22	co 7255	. . . . . . . 8 class ((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢)
24	23, 16	cgox 33300	. . . . . . 7 class ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢)
25		cgob 33298	. . . . . . 7 class ↔𝑔
26	19, 24, 25	co 7255	. . . . . 6 class ((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢))
27	26, 9	cgol 33197	. . . . 5 class ∀𝑔2o((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢))
28	27, 7	cgol 33197	. . . 4 class ∀𝑔1o∀𝑔2o((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢))
29	17, 28, 12	co 7255	. . 3 class (∀𝑔3o∃𝑔1o∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o)) →𝑔 ∀𝑔1o∀𝑔2o((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢)))
30	2, 5, 29	cmpt 5153	. 2 class (𝑢 ∈ (Fmla‘ω) ↦ (∀𝑔3o∃𝑔1o∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o)) →𝑔 ∀𝑔1o∀𝑔2o((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢))))
31	1, 30	wceq 1539	1 wff AxRep = (𝑢 ∈ (Fmla‘ω) ↦ (∀𝑔3o∃𝑔1o∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o)) →𝑔 ∀𝑔1o∀𝑔2o((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢))))

This definition is referenced by: (None)