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

Definition df-fo 195
Description: Define an onto function. (Contributed by Mario Carneiro, 10-Oct-2014.)
Assertion
Ref Expression
df-fo |- T. |= [onto = \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))]
Distinct variable group:   x,f,y

Detailed syntax breakdown of Definition df-fo
StepHypRef Expression
1 kt 8 . 2 term T.
2 tfo 190 . . 3 term onto
3 hal . . . . 5 type al
4 hbe . . . . 5 type be
53, 4ht 2 . . . 4 type (al -> be)
6 vf . . . 4 var f
7 tal 122 . . . . 5 term A.
8 vy . . . . . 6 var y
9 tex 123 . . . . . . 7 term E.
10 vx . . . . . . . 8 var x
114, 8tv 1 . . . . . . . . 9 term y:be
125, 6tv 1 . . . . . . . . . 10 term f:(al -> be)
133, 10tv 1 . . . . . . . . . 10 term x:al
1412, 13kc 5 . . . . . . . . 9 term (f:(al -> be)x:al)
15 ke 7 . . . . . . . . 9 term =
1611, 14, 15kbr 9 . . . . . . . 8 term [y:be = (f:(al -> be)x:al)]
173, 10, 16kl 6 . . . . . . 7 term \x:al [y:be = (f:(al -> be)x:al)]
189, 17kc 5 . . . . . 6 term (E.\x:al [y:be = (f:(al -> be)x:al)])
194, 8, 18kl 6 . . . . 5 term \y:be (E.\x:al [y:be = (f:(al -> be)x:al)])
207, 19kc 5 . . . 4 term (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))
215, 6, 20kl 6 . . 3 term \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))
222, 21, 15kbr 9 . 2 term [onto = \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))]
231, 22wffMMJ2 11 1 wff T. |= [onto = \f:(al -> be) (A.\y:be (E.\x:al [y:be = (f:(al -> be)x:al)]))]
Colors of variables: type var term
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator