Definition df-gzrep 33416

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 33409	. 2 class AxRep
2		vu	. . 3 setvar 𝑢
3		com 7712	. . . 4 class ω
4		cfmla 33299	. . . 4 class Fmla
5	3, 4	cfv 6433	. . 3 class (Fmla‘ω)
6	2	cv 1538	. . . . . . . . 9 class 𝑢
7		c1o 8290	. . . . . . . . 9 class 1o
8	6, 7	cgol 33297	. . . . . . . 8 class ∀𝑔1o𝑢
9		c2o 8291	. . . . . . . . 9 class 2o
10		cgoq 33399	. . . . . . . . 9 class =𝑔
11	9, 7, 10	co 7275	. . . . . . . 8 class (2o=𝑔1o)
12		cgoi 33396	. . . . . . . 8 class →𝑔
13	8, 11, 12	co 7275	. . . . . . 7 class (∀𝑔1o𝑢 →𝑔 (2o=𝑔1o))
14	13, 9	cgol 33297	. . . . . 6 class ∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o))
15	14, 7	cgox 33400	. . . . 5 class ∃𝑔1o∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o))
16		c3o 8292	. . . . 5 class 3o
17	15, 16	cgol 33297	. . . 4 class ∀𝑔3o∃𝑔1o∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o))
18		cgoe 33295	. . . . . . . 8 class ∈𝑔
19	9, 7, 18	co 7275	. . . . . . 7 class (2o∈𝑔1o)
20		c0 4256	. . . . . . . . . 10 class ∅
21	16, 20, 18	co 7275	. . . . . . . . 9 class (3o∈𝑔∅)
22		cgoa 33395	. . . . . . . . 9 class ∧𝑔
23	21, 8, 22	co 7275	. . . . . . . 8 class ((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢)
24	23, 16	cgox 33400	. . . . . . 7 class ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢)
25		cgob 33398	. . . . . . 7 class ↔𝑔
26	19, 24, 25	co 7275	. . . . . 6 class ((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢))
27	26, 9	cgol 33297	. . . . 5 class ∀𝑔2o((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢))
28	27, 7	cgol 33297	. . . 4 class ∀𝑔1o∀𝑔2o((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢))
29	17, 28, 12	co 7275	. . 3 class (∀𝑔3o∃𝑔1o∀𝑔2o(∀𝑔1o𝑢 →𝑔 (2o=𝑔1o)) →𝑔 ∀𝑔1o∀𝑔2o((2o∈𝑔1o) ↔𝑔 ∃𝑔3o((3o∈𝑔∅)∧𝑔∀𝑔1o𝑢)))
30	2, 5, 29	cmpt 5157	. 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)