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

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
StepHypRef Expression
1 kt 8 . 2 term
2 tf11 189 . . 3 term 1-1
3 hal . . . . 5 type α
4 hbe . . . . 5 type β
53, 4ht 2 . . . 4 type (αβ)
6 vf . . . 4 var f
7 tal 122 . . . . 5 term
8 vx . . . . . 6 var x
9 vy . . . . . . . 8 var y
105, 6tv 1 . . . . . . . . . . 11 term f:(αβ)
113, 8tv 1 . . . . . . . . . . 11 term x:α
1210, 11kc 5 . . . . . . . . . 10 term (f:(αβ)x:α)
133, 9tv 1 . . . . . . . . . . 11 term y:α
1410, 13kc 5 . . . . . . . . . 10 term (f:(αβ)y:α)
15 ke 7 . . . . . . . . . 10 term =
1612, 14, 15kbr 9 . . . . . . . . 9 term [(f:(αβ)x:α) = (f:(αβ)y:α)]
1711, 13, 15kbr 9 . . . . . . . . 9 term [x:α = y:α]
18 tim 121 . . . . . . . . 9 term
1916, 17, 18kbr 9 . . . . . . . 8 term [[(f:(αβ)x:α) = (f:(αβ)y:α)] ⇒ [x:α = y:α]]
203, 9, 19kl 6 . . . . . . 7 term λy:α [[(f:(αβ)x:α) = (f:(αβ)y:α)] ⇒ [x:α = y:α]]
217, 20kc 5 . . . . . 6 term (λy:α [[(f:(αβ)x:α) = (f:(αβ)y:α)] ⇒ [x:α = y:α]])
223, 8, 21kl 6 . . . . 5 term λx:α (λy:α [[(f:(αβ)x:α) = (f:(αβ)y:α)] ⇒ [x:α = y:α]])
237, 22kc 5 . . . 4 term (λx:α (λy:α [[(f:(αβ)x:α) = (f:(αβ)y:α)] ⇒ [x:α = y:α]]))
245, 6, 23kl 6 . . 3 term λf:(αβ) (λx:α (λy:α [[(f:(αβ)x:α) = (f:(αβ)y:α)] ⇒ [x:α = y:α]]))
252, 24, 15kbr 9 . 2 term [1-1 = λf:(αβ) (λx:α (λy:α [[(f:(αβ)x:α) = (f:(αβ)y:α)] ⇒ [x:α = y:α]]))]
261, 25wffMMJ2 11 1 wff ⊤⊧[1-1 = λf:(αβ) (λx:α (λy:α [[(f:(αβ)x:α) = (f:(αβ)y:α)] ⇒ [x:α = y:α]]))]
Colors of variables: type var term
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator