Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gzreg Structured version   Visualization version   GIF version

Definition df-gzreg 32761
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
StepHypRef Expression
1 cgzg 32754 . 2 class AxReg
2 c1o 8091 . . . . 5 class 1o
3 c0 4276 . . . . 5 class
4 cgoe 32637 . . . . 5 class 𝑔
52, 3, 4co 7149 . . . 4 class (1o𝑔∅)
65, 2cgox 32742 . . 3 class 𝑔1o(1o𝑔∅)
7 c2o 8092 . . . . . . . 8 class 2o
87, 2, 4co 7149 . . . . . . 7 class (2o𝑔1o)
97, 3, 4co 7149 . . . . . . . 8 class (2o𝑔∅)
109cgon 32736 . . . . . . 7 class ¬𝑔(2o𝑔∅)
11 cgoi 32738 . . . . . . 7 class 𝑔
128, 10, 11co 7149 . . . . . 6 class ((2o𝑔1o) →𝑔 ¬𝑔(2o𝑔∅))
1312, 7cgol 32639 . . . . 5 class 𝑔2o((2o𝑔1o) →𝑔 ¬𝑔(2o𝑔∅))
14 cgoa 32737 . . . . 5 class 𝑔
155, 13, 14co 7149 . . . 4 class ((1o𝑔∅)∧𝑔𝑔2o((2o𝑔1o) →𝑔 ¬𝑔(2o𝑔∅)))
1615, 2cgox 32742 . . 3 class 𝑔1o((1o𝑔∅)∧𝑔𝑔2o((2o𝑔1o) →𝑔 ¬𝑔(2o𝑔∅)))
176, 16, 11co 7149 . 2 class (∃𝑔1o(1o𝑔∅) →𝑔𝑔1o((1o𝑔∅)∧𝑔𝑔2o((2o𝑔1o) →𝑔 ¬𝑔(2o𝑔∅))))
181, 17wceq 1538 1 wff AxReg = (∃𝑔1o(1o𝑔∅) →𝑔𝑔1o((1o𝑔∅)∧𝑔𝑔2o((2o𝑔1o) →𝑔 ¬𝑔(2o𝑔∅))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator