Definition df-gzinf

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgzi	⊢ AxInf
1		c1o	⊢ 1o
2		c0	⊢ ∅
3		cgoe	⊢ ∈𝑔
4	2 1 3	co	⊢ ( ∅ ∈𝑔 1o )
5		cgoa	⊢ ∧𝑔
6		c2o	⊢ 2o
7	6 1 3	co	⊢ ( 2o ∈𝑔 1o )
8		cgoi	⊢ →𝑔
9	6 2 3	co	⊢ ( 2o ∈𝑔 ∅ )
10	9 4 5	co	⊢ ( ( 2o ∈𝑔 ∅ ) ∧𝑔 ( ∅ ∈𝑔 1o ) )
11	10 2	cgox	⊢ ∃𝑔 ∅ ( ( 2o ∈𝑔 ∅ ) ∧𝑔 ( ∅ ∈𝑔 1o ) )
12	7 11 8	co	⊢ ( ( 2o ∈𝑔 1o ) →𝑔 ∃𝑔 ∅ ( ( 2o ∈𝑔 ∅ ) ∧𝑔 ( ∅ ∈𝑔 1o ) ) )
13	12 6	cgol	⊢ ∀𝑔 2o ( ( 2o ∈𝑔 1o ) →𝑔 ∃𝑔 ∅ ( ( 2o ∈𝑔 ∅ ) ∧𝑔 ( ∅ ∈𝑔 1o ) ) )
14	4 13 5	co	⊢ ( ( ∅ ∈𝑔 1o ) ∧𝑔 ∀𝑔 2o ( ( 2o ∈𝑔 1o ) →𝑔 ∃𝑔 ∅ ( ( 2o ∈𝑔 ∅ ) ∧𝑔 ( ∅ ∈𝑔 1o ) ) ) )
15	14 1	cgox	⊢ ∃𝑔 1o ( ( ∅ ∈𝑔 1o ) ∧𝑔 ∀𝑔 2o ( ( 2o ∈𝑔 1o ) →𝑔 ∃𝑔 ∅ ( ( 2o ∈𝑔 ∅ ) ∧𝑔 ( ∅ ∈𝑔 1o ) ) ) )
16	0 15	wceq	⊢ AxInf = ∃𝑔 1o ( ( ∅ ∈𝑔 1o ) ∧𝑔 ∀𝑔 2o ( ( 2o ∈𝑔 1o ) →𝑔 ∃𝑔 ∅ ( ( 2o ∈𝑔 ∅ ) ∧𝑔 ( ∅ ∈𝑔 1o ) ) ) )