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 32758
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 32751 . 2 class AxRep
2 vu . . 3 setvar 𝑢
3 com 7574 . . . 4 class ω
4 cfmla 32641 . . . 4 class Fmla
53, 4cfv 6343 . . 3 class (Fmla‘ω)
62cv 1537 . . . . . . . . 9 class 𝑢
7 c1o 8091 . . . . . . . . 9 class 1o
86, 7cgol 32639 . . . . . . . 8 class 𝑔1o𝑢
9 c2o 8092 . . . . . . . . 9 class 2o
10 cgoq 32741 . . . . . . . . 9 class =𝑔
119, 7, 10co 7149 . . . . . . . 8 class (2o=𝑔1o)
12 cgoi 32738 . . . . . . . 8 class 𝑔
138, 11, 12co 7149 . . . . . . 7 class (∀𝑔1o𝑢𝑔 (2o=𝑔1o))
1413, 9cgol 32639 . . . . . 6 class 𝑔2o(∀𝑔1o𝑢𝑔 (2o=𝑔1o))
1514, 7cgox 32742 . . . . 5 class 𝑔1o𝑔2o(∀𝑔1o𝑢𝑔 (2o=𝑔1o))
16 c3o 8093 . . . . 5 class 3o
1715, 16cgol 32639 . . . 4 class 𝑔3o𝑔1o𝑔2o(∀𝑔1o𝑢𝑔 (2o=𝑔1o))
18 cgoe 32637 . . . . . . . 8 class 𝑔
199, 7, 18co 7149 . . . . . . 7 class (2o𝑔1o)
20 c0 4276 . . . . . . . . . 10 class
2116, 20, 18co 7149 . . . . . . . . 9 class (3o𝑔∅)
22 cgoa 32737 . . . . . . . . 9 class 𝑔
2321, 8, 22co 7149 . . . . . . . 8 class ((3o𝑔∅)∧𝑔𝑔1o𝑢)
2423, 16cgox 32742 . . . . . . 7 class 𝑔3o((3o𝑔∅)∧𝑔𝑔1o𝑢)
25 cgob 32740 . . . . . . 7 class 𝑔
2619, 24, 25co 7149 . . . . . 6 class ((2o𝑔1o) ↔𝑔𝑔3o((3o𝑔∅)∧𝑔𝑔1o𝑢))
2726, 9cgol 32639 . . . . 5 class 𝑔2o((2o𝑔1o) ↔𝑔𝑔3o((3o𝑔∅)∧𝑔𝑔1o𝑢))
2827, 7cgol 32639 . . . 4 class 𝑔1o𝑔2o((2o𝑔1o) ↔𝑔𝑔3o((3o𝑔∅)∧𝑔𝑔1o𝑢))
2917, 28, 12co 7149 . . 3 class (∀𝑔3o𝑔1o𝑔2o(∀𝑔1o𝑢𝑔 (2o=𝑔1o)) →𝑔𝑔1o𝑔2o((2o𝑔1o) ↔𝑔𝑔3o((3o𝑔∅)∧𝑔𝑔1o𝑢)))
302, 5, 29cmpt 5132 . 2 class (𝑢 ∈ (Fmla‘ω) ↦ (∀𝑔3o𝑔1o𝑔2o(∀𝑔1o𝑢𝑔 (2o=𝑔1o)) →𝑔𝑔1o𝑔2o((2o𝑔1o) ↔𝑔𝑔3o((3o𝑔∅)∧𝑔𝑔1o𝑢))))
311, 30wceq 1538 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