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

Step	Hyp	Ref	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
7	3, 4	tv 1	. . . . . . . 8 term x:be
8	6, 7	kc 5	. . . . . . 7 term (Rx:be)
9	5, 8	kc 5	. . . . . 6 term (A(Rx:be))
10		ke 7	. . . . . 6 term =
11	9, 7, 10	kbr 9	. . . . 5 term [(A(Rx:be)) = x:be]
12	3, 4, 11	kl 6	. . . 4 term \x:be [(A(Rx:be)) = x:be]
13	2, 12	kc 5	. . 3 term (A.\x:be [(A(Rx:be)) = x:be])
14		hal	. . . . 5 type al
15		tf	. . . . . . 7 term F
16	14, 4	tv 1	. . . . . . 7 term x:al
17	15, 16	kc 5	. . . . . 6 term (Fx:al)
18	5, 16	kc 5	. . . . . . . 8 term (Ax:al)
19	6, 18	kc 5	. . . . . . 7 term (R(Ax:al))
20	19, 16, 10	kbr 9	. . . . . 6 term [(R(Ax:al)) = x:al]
21	17, 20, 10	kbr 9	. . . . 5 term [(Fx:al) = [(R(Ax:al)) = x:al]]
22	14, 4, 21	kl 6	. . . 4 term \x:al [(Fx:al) = [(R(Ax:al)) = x:al]]
23	2, 22	kc 5	. . 3 term (A.\x:al [(Fx:al) = [(R(Ax:al)) = x:al]])
24	13, 23	kct 10	. 2 term ((A.\x:be [(A(Rx:be)) = x:be]), (A.\x:al [(Fx:al) = [(R(Ax:al)) = x:al]]))
25	1, 24	wffMMJ2 11	1 wff T. |= ((A.\x:be [(A(Rx:be)) = x:be]), (A.\x:al [(Fx:al) = [(R(Ax:al)) = x:al]]))

This axiom is referenced by: (None)