Definition df-gzreg 33319

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

Assertion

Ref	Expression
df-gzreg	⊢ AxReg = (∃𝑔1o(1o∈𝑔∅) →𝑔 ∃𝑔1o((1o∈𝑔∅)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ¬𝑔(2o∈𝑔∅))))

Detailed syntax breakdown of Definition df-gzreg

Step	Hyp	Ref	Expression
1		cgzg 33312	. 2 class AxReg
2		c1o 8260	. . . . 5 class 1o
3		c0 4253	. . . . 5 class ∅
4		cgoe 33195	. . . . 5 class ∈𝑔
5	2, 3, 4	co 7255	. . . 4 class (1o∈𝑔∅)
6	5, 2	cgox 33300	. . 3 class ∃𝑔1o(1o∈𝑔∅)
7		c2o 8261	. . . . . . . 8 class 2o
8	7, 2, 4	co 7255	. . . . . . 7 class (2o∈𝑔1o)
9	7, 3, 4	co 7255	. . . . . . . 8 class (2o∈𝑔∅)
10	9	cgon 33294	. . . . . . 7 class ¬𝑔(2o∈𝑔∅)
11		cgoi 33296	. . . . . . 7 class →𝑔
12	8, 10, 11	co 7255	. . . . . 6 class ((2o∈𝑔1o) →𝑔 ¬𝑔(2o∈𝑔∅))
13	12, 7	cgol 33197	. . . . 5 class ∀𝑔2o((2o∈𝑔1o) →𝑔 ¬𝑔(2o∈𝑔∅))
14		cgoa 33295	. . . . 5 class ∧𝑔
15	5, 13, 14	co 7255	. . . 4 class ((1o∈𝑔∅)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ¬𝑔(2o∈𝑔∅)))
16	15, 2	cgox 33300	. . 3 class ∃𝑔1o((1o∈𝑔∅)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ¬𝑔(2o∈𝑔∅)))
17	6, 16, 11	co 7255	. 2 class (∃𝑔1o(1o∈𝑔∅) →𝑔 ∃𝑔1o((1o∈𝑔∅)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ¬𝑔(2o∈𝑔∅))))
18	1, 17	wceq 1539	1 wff AxReg = (∃𝑔1o(1o∈𝑔∅) →𝑔 ∃𝑔1o((1o∈𝑔∅)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ¬𝑔(2o∈𝑔∅))))

This definition is referenced by: (None)