Definition df-gzreg

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

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

Detailed syntax breakdown

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