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

Axiom ax-tdef 176
Description: The type definition axiom. The last hypothesis corresponds to the actual definition one wants to make; here we are defining a new type be and the definition will provide us with pair of bijections A, R mapping the new type be to the subset of the old type al such that Fx is true. In order for this to be a valid (conservative) extension, we must ensure that the new type is nonempty, and for that purpose we need a witness B that F is not always false. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
ax-tdef.1 |- B:al
ax-tdef.2 |- F:(al -> *)
ax-tdef.3 |- T. |= (FB)
ax-tdef.4 |- typedef be(A, R)F
Assertion
Ref Expression
ax-tdef |- T. |= ((A.\x:be [(A(Rx:be)) = x:be]), (A.\x:al [(Fx:al) = [(R(Ax:al)) = x:al]]))
Distinct variable groups:   x,A   x,R   x,F

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