Definition df-f11 194

Description: Define a one-to-one function. (Contributed by Mario Carneiro, 10-Oct-2014.)

Assertion

Ref	Expression
df-f11	⊢ ⊤⊧[1-1 = λf:(α → β) (∀λx:α (∀λy:α [[(f:(α → β)x:α) = (f:(α → β)y:α)] ⇒ [x:α = y:α]]))]

Distinct variable group:   x,f,y

Detailed syntax breakdown of Definition df-f11

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		tf11 189	. . 3 term 1-1
3		hal	. . . . 5 type α
4		hbe	. . . . 5 type β
5	3, 4	ht 2	. . . 4 type (α → β)
6		vf	. . . 4 var f
7		tal 122	. . . . 5 term ∀
8		vx	. . . . . 6 var x
9		vy	. . . . . . . 8 var y
10	5, 6	tv 1	. . . . . . . . . . 11 term f:(α → β)
11	3, 8	tv 1	. . . . . . . . . . 11 term x:α
12	10, 11	kc 5	. . . . . . . . . 10 term (f:(α → β)x:α)
13	3, 9	tv 1	. . . . . . . . . . 11 term y:α
14	10, 13	kc 5	. . . . . . . . . 10 term (f:(α → β)y:α)
15		ke 7	. . . . . . . . . 10 term =
16	12, 14, 15	kbr 9	. . . . . . . . 9 term [(f:(α → β)x:α) = (f:(α → β)y:α)]
17	11, 13, 15	kbr 9	. . . . . . . . 9 term [x:α = y:α]
18		tim 121	. . . . . . . . 9 term ⇒
19	16, 17, 18	kbr 9	. . . . . . . 8 term [[(f:(α → β)x:α) = (f:(α → β)y:α)] ⇒ [x:α = y:α]]
20	3, 9, 19	kl 6	. . . . . . 7 term λy:α [[(f:(α → β)x:α) = (f:(α → β)y:α)] ⇒ [x:α = y:α]]
21	7, 20	kc 5	. . . . . 6 term (∀λy:α [[(f:(α → β)x:α) = (f:(α → β)y:α)] ⇒ [x:α = y:α]])
22	3, 8, 21	kl 6	. . . . 5 term λx:α (∀λy:α [[(f:(α → β)x:α) = (f:(α → β)y:α)] ⇒ [x:α = y:α]])
23	7, 22	kc 5	. . . 4 term (∀λx:α (∀λy:α [[(f:(α → β)x:α) = (f:(α → β)y:α)] ⇒ [x:α = y:α]]))
24	5, 6, 23	kl 6	. . 3 term λf:(α → β) (∀λx:α (∀λy:α [[(f:(α → β)x:α) = (f:(α → β)y:α)] ⇒ [x:α = y:α]]))
25	2, 24, 15	kbr 9	. 2 term [1-1 = λf:(α → β) (∀λx:α (∀λy:α [[(f:(α → β)x:α) = (f:(α → β)y:α)] ⇒ [x:α = y:α]]))]
26	1, 25	wffMMJ2 11	1 wff ⊤⊧[1-1 = λf:(α → β) (∀λx:α (∀λy:α [[(f:(α → β)x:α) = (f:(α → β)y:α)] ⇒ [x:α = y:α]]))]

This definition is referenced by: (None)