Definition df-gzinf 35463

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

Assertion

Ref	Expression
df-gzinf	⊢ AxInf = ∃𝑔1o((∅∈𝑔1o)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ∃𝑔∅((2o∈𝑔∅)∧𝑔(∅∈𝑔1o))))

Detailed syntax breakdown of Definition df-gzinf

Step	Hyp	Ref	Expression
1		cgzi 35456	. 2 class AxInf
2		c0 4333	. . . . 5 class ∅
3		c1o 8499	. . . . 5 class 1o
4		cgoe 35338	. . . . 5 class ∈𝑔
5	2, 3, 4	co 7431	. . . 4 class (∅∈𝑔1o)
6		c2o 8500	. . . . . . 7 class 2o
7	6, 3, 4	co 7431	. . . . . 6 class (2o∈𝑔1o)
8	6, 2, 4	co 7431	. . . . . . . 8 class (2o∈𝑔∅)
9		cgoa 35438	. . . . . . . 8 class ∧𝑔
10	8, 5, 9	co 7431	. . . . . . 7 class ((2o∈𝑔∅)∧𝑔(∅∈𝑔1o))
11	10, 2	cgox 35443	. . . . . 6 class ∃𝑔∅((2o∈𝑔∅)∧𝑔(∅∈𝑔1o))
12		cgoi 35439	. . . . . 6 class →𝑔
13	7, 11, 12	co 7431	. . . . 5 class ((2o∈𝑔1o) →𝑔 ∃𝑔∅((2o∈𝑔∅)∧𝑔(∅∈𝑔1o)))
14	13, 6	cgol 35340	. . . 4 class ∀𝑔2o((2o∈𝑔1o) →𝑔 ∃𝑔∅((2o∈𝑔∅)∧𝑔(∅∈𝑔1o)))
15	5, 14, 9	co 7431	. . 3 class ((∅∈𝑔1o)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ∃𝑔∅((2o∈𝑔∅)∧𝑔(∅∈𝑔1o))))
16	15, 3	cgox 35443	. 2 class ∃𝑔1o((∅∈𝑔1o)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ∃𝑔∅((2o∈𝑔∅)∧𝑔(∅∈𝑔1o))))
17	1, 16	wceq 1540	1 wff AxInf = ∃𝑔1o((∅∈𝑔1o)∧𝑔∀𝑔2o((2o∈𝑔1o) →𝑔 ∃𝑔∅((2o∈𝑔∅)∧𝑔(∅∈𝑔1o))))

This definition is referenced by: (None)