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

Definition df-gzrep 34112
Description: The Godel-set version of the Axiom Scheme of Replacement. Since this is a scheme and not a single axiom, it manifests as a function on wffs, each giving rise to a different axiom. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gzrep AxRep = (𝑒 ∈ (Fmlaβ€˜Ο‰) ↦ (βˆ€π‘”3oβˆƒπ‘”1oβˆ€π‘”2o(βˆ€π‘”1o𝑒 →𝑔 (2o=𝑔1o)) →𝑔 βˆ€π‘”1oβˆ€π‘”2o((2oβˆˆπ‘”1o) ↔𝑔 βˆƒπ‘”3o((3oβˆˆπ‘”βˆ…)βˆ§π‘”βˆ€π‘”1o𝑒))))

Detailed syntax breakdown of Definition df-gzrep
StepHypRef Expression
1 cgzr 34105 . 2 class AxRep
2 vu . . 3 setvar 𝑒
3 com 7806 . . . 4 class Ο‰
4 cfmla 33995 . . . 4 class Fmla
53, 4cfv 6500 . . 3 class (Fmlaβ€˜Ο‰)
62cv 1541 . . . . . . . . 9 class 𝑒
7 c1o 8409 . . . . . . . . 9 class 1o
86, 7cgol 33993 . . . . . . . 8 class βˆ€π‘”1o𝑒
9 c2o 8410 . . . . . . . . 9 class 2o
10 cgoq 34095 . . . . . . . . 9 class =𝑔
119, 7, 10co 7361 . . . . . . . 8 class (2o=𝑔1o)
12 cgoi 34092 . . . . . . . 8 class →𝑔
138, 11, 12co 7361 . . . . . . 7 class (βˆ€π‘”1o𝑒 →𝑔 (2o=𝑔1o))
1413, 9cgol 33993 . . . . . 6 class βˆ€π‘”2o(βˆ€π‘”1o𝑒 →𝑔 (2o=𝑔1o))
1514, 7cgox 34096 . . . . 5 class βˆƒπ‘”1oβˆ€π‘”2o(βˆ€π‘”1o𝑒 →𝑔 (2o=𝑔1o))
16 c3o 8411 . . . . 5 class 3o
1715, 16cgol 33993 . . . 4 class βˆ€π‘”3oβˆƒπ‘”1oβˆ€π‘”2o(βˆ€π‘”1o𝑒 →𝑔 (2o=𝑔1o))
18 cgoe 33991 . . . . . . . 8 class βˆˆπ‘”
199, 7, 18co 7361 . . . . . . 7 class (2oβˆˆπ‘”1o)
20 c0 4286 . . . . . . . . . 10 class βˆ…
2116, 20, 18co 7361 . . . . . . . . 9 class (3oβˆˆπ‘”βˆ…)
22 cgoa 34091 . . . . . . . . 9 class βˆ§π‘”
2321, 8, 22co 7361 . . . . . . . 8 class ((3oβˆˆπ‘”βˆ…)βˆ§π‘”βˆ€π‘”1o𝑒)
2423, 16cgox 34096 . . . . . . 7 class βˆƒπ‘”3o((3oβˆˆπ‘”βˆ…)βˆ§π‘”βˆ€π‘”1o𝑒)
25 cgob 34094 . . . . . . 7 class ↔𝑔
2619, 24, 25co 7361 . . . . . 6 class ((2oβˆˆπ‘”1o) ↔𝑔 βˆƒπ‘”3o((3oβˆˆπ‘”βˆ…)βˆ§π‘”βˆ€π‘”1o𝑒))
2726, 9cgol 33993 . . . . 5 class βˆ€π‘”2o((2oβˆˆπ‘”1o) ↔𝑔 βˆƒπ‘”3o((3oβˆˆπ‘”βˆ…)βˆ§π‘”βˆ€π‘”1o𝑒))
2827, 7cgol 33993 . . . 4 class βˆ€π‘”1oβˆ€π‘”2o((2oβˆˆπ‘”1o) ↔𝑔 βˆƒπ‘”3o((3oβˆˆπ‘”βˆ…)βˆ§π‘”βˆ€π‘”1o𝑒))
2917, 28, 12co 7361 . . 3 class (βˆ€π‘”3oβˆƒπ‘”1oβˆ€π‘”2o(βˆ€π‘”1o𝑒 →𝑔 (2o=𝑔1o)) →𝑔 βˆ€π‘”1oβˆ€π‘”2o((2oβˆˆπ‘”1o) ↔𝑔 βˆƒπ‘”3o((3oβˆˆπ‘”βˆ…)βˆ§π‘”βˆ€π‘”1o𝑒)))
302, 5, 29cmpt 5192 . 2 class (𝑒 ∈ (Fmlaβ€˜Ο‰) ↦ (βˆ€π‘”3oβˆƒπ‘”1oβˆ€π‘”2o(βˆ€π‘”1o𝑒 →𝑔 (2o=𝑔1o)) →𝑔 βˆ€π‘”1oβˆ€π‘”2o((2oβˆˆπ‘”1o) ↔𝑔 βˆƒπ‘”3o((3oβˆˆπ‘”βˆ…)βˆ§π‘”βˆ€π‘”1o𝑒))))
311, 30wceq 1542 1 wff AxRep = (𝑒 ∈ (Fmlaβ€˜Ο‰) ↦ (βˆ€π‘”3oβˆƒπ‘”1oβˆ€π‘”2o(βˆ€π‘”1o𝑒 →𝑔 (2o=𝑔1o)) →𝑔 βˆ€π‘”1oβˆ€π‘”2o((2oβˆˆπ‘”1o) ↔𝑔 βˆƒπ‘”3o((3oβˆˆπ‘”βˆ…)βˆ§π‘”βˆ€π‘”1o𝑒))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator