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

Definition df-gzinf 31687
Description: The Godel-set version of the Axiom of Infinity. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzinf AxInf = ∃𝑔1𝑜((∅∈𝑔1𝑜)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))))

Detailed syntax breakdown of Definition df-gzinf
StepHypRef Expression
1 cgzi 31680 . 2 class AxInf
2 c0 4061 . . . . 5 class
3 c1o 7705 . . . . 5 class 1𝑜
4 cgoe 31647 . . . . 5 class 𝑔
52, 3, 4co 6792 . . . 4 class (∅∈𝑔1𝑜)
6 c2o 7706 . . . . . . 7 class 2𝑜
76, 3, 4co 6792 . . . . . 6 class (2𝑜𝑔1𝑜)
86, 2, 4co 6792 . . . . . . . 8 class (2𝑜𝑔∅)
9 cgoa 31661 . . . . . . . 8 class 𝑔
108, 5, 9co 6792 . . . . . . 7 class ((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))
1110, 2cgox 31666 . . . . . 6 class 𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))
12 cgoi 31662 . . . . . 6 class 𝑔
137, 11, 12co 6792 . . . . 5 class ((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜)))
1413, 6cgol 31649 . . . 4 class 𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜)))
155, 14, 9co 6792 . . 3 class ((∅∈𝑔1𝑜)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))))
1615, 3cgox 31666 . 2 class 𝑔1𝑜((∅∈𝑔1𝑜)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))))
171, 16wceq 1630 1 wff AxInf = ∃𝑔1𝑜((∅∈𝑔1𝑜)∧𝑔𝑔2𝑜((2𝑜𝑔1𝑜) →𝑔𝑔∅((2𝑜𝑔∅)∧𝑔(∅∈𝑔1𝑜))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator