Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-tdef GIF version

Axiom ax-tdef 164
 Description: The type definition axiom. The last hypothesis corresponds to the actual definition one wants to make; here we are defining a new type β and the definition will provide us with pair of bijections A, R mapping the new type β to the subset of the old type α such that Fx is true. In order for this to be a valid (conservative) extension, we must ensure that the new type is non-empty, and for that purpose we need a witness B that F is not always false.
Hypotheses
Ref Expression
ax-tdef.1 B:α
ax-tdef.2 F:(α → ∗)
ax-tdef.3 ⊤⊧(FB)
ax-tdef.4 typedef β(A, R)F
Assertion
Ref Expression
ax-tdef ⊤⊧((λx:β [(A(Rx:β)) = x:β]), (λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]))
Distinct variable groups:   x,A   x,R   x,F

Detailed syntax breakdown of Axiom ax-tdef
StepHypRef Expression
1 kt 8 . 2 term
2 tal 112 . . . 4 term
3 hbe . . . . 5 type β
4 vx . . . . 5 var x
5 ta . . . . . . 7 term A
6 tr . . . . . . . 8 term R
73, 4tv 1 . . . . . . . 8 term x:β
86, 7kc 5 . . . . . . 7 term (Rx:β)
95, 8kc 5 . . . . . 6 term (A(Rx:β))
10 ke 7 . . . . . 6 term =
119, 7, 10kbr 9 . . . . 5 term [(A(Rx:β)) = x:β]
123, 4, 11kl 6 . . . 4 term λx:β [(A(Rx:β)) = x:β]
132, 12kc 5 . . 3 term (λx:β [(A(Rx:β)) = x:β])
14 hal . . . . 5 type α
15 tf . . . . . . 7 term F
1614, 4tv 1 . . . . . . 7 term x:α
1715, 16kc 5 . . . . . 6 term (Fx:α)
185, 16kc 5 . . . . . . . 8 term (Ax:α)
196, 18kc 5 . . . . . . 7 term (R(Ax:α))
2019, 16, 10kbr 9 . . . . . 6 term [(R(Ax:α)) = x:α]
2117, 20, 10kbr 9 . . . . 5 term [(Fx:α) = [(R(Ax:α)) = x:α]]
2214, 4, 21kl 6 . . . 4 term λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]
232, 22kc 5 . . 3 term (λx:α [(Fx:α) = [(R(Ax:α)) = x:α]])
2413, 23kct 10 . 2 term ((λx:β [(A(Rx:β)) = x:β]), (λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]))
251, 24wffMMJ2 11 1 wff ⊤⊧((λx:β [(A(Rx:β)) = x:β]), (λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]))
 Colors of variables: type var term This axiom is referenced by: (None)
 Copyright terms: Public domain W3C validator