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 β 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 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:α
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

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		tal 122	. . . 4 term ∀
3		hbe	. . . . 5 type β
4		vx	. . . . 5 var x
5		ta	. . . . . . 7 term A
6		tr	. . . . . . . 8 term R
7	3, 4	tv 1	. . . . . . . 8 term x:β
8	6, 7	kc 5	. . . . . . 7 term (Rx:β)
9	5, 8	kc 5	. . . . . 6 term (A(Rx:β))
10		ke 7	. . . . . 6 term =
11	9, 7, 10	kbr 9	. . . . 5 term [(A(Rx:β)) = x:β]
12	3, 4, 11	kl 6	. . . 4 term λx:β [(A(Rx:β)) = x:β]
13	2, 12	kc 5	. . 3 term (∀λx:β [(A(Rx:β)) = x:β])
14		hal	. . . . 5 type α
15		tf	. . . . . . 7 term F
16	14, 4	tv 1	. . . . . . 7 term x:α
17	15, 16	kc 5	. . . . . 6 term (Fx:α)
18	5, 16	kc 5	. . . . . . . 8 term (Ax:α)
19	6, 18	kc 5	. . . . . . 7 term (R(Ax:α))
20	19, 16, 10	kbr 9	. . . . . 6 term [(R(Ax:α)) = x:α]
21	17, 20, 10	kbr 9	. . . . 5 term [(Fx:α) = [(R(Ax:α)) = x:α]]
22	14, 4, 21	kl 6	. . . 4 term λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]
23	2, 22	kc 5	. . 3 term (∀λx:α [(Fx:α) = [(R(Ax:α)) = x:α]])
24	13, 23	kct 10	. 2 term ((∀λx:β [(A(Rx:β)) = x:β]), (∀λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]))
25	1, 24	wffMMJ2 11	1 wff ⊤⊧((∀λx:β [(A(Rx:β)) = x:β]), (∀λx:α [(Fx:α) = [(R(Ax:α)) = x:α]]))

This axiom is referenced by: (None)