Detailed syntax breakdown of Definition df-f11
Step | Hyp | Ref
| Expression |
1 | | kt 8 |
. 2
term ![T.](top.gif) |
2 | | tf11 189 |
. . 3
term 1-1 |
3 | | hal |
. . . . 5
type ![al](_alpha.gif) |
4 | | hbe |
. . . . 5
type ![be](_beta.gif) |
5 | 3, 4 | ht 2 |
. . . 4
type ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) |
6 | | vf |
. . . 4
var ![f](_f.gif) |
7 | | tal 122 |
. . . . 5
term ![A.](forall.gif) |
8 | | vx |
. . . . . 6
var ![x](_x.gif) |
9 | | vy |
. . . . . . . 8
var ![y](_y.gif) |
10 | 5, 6 | tv 1 |
. . . . . . . . . . 11
term ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) |
11 | 3, 8 | tv 1 |
. . . . . . . . . . 11
term ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) |
12 | 10, 11 | kc 5 |
. . . . . . . . . 10
term ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) |
13 | 3, 9 | tv 1 |
. . . . . . . . . . 11
term ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) |
14 | 10, 13 | kc 5 |
. . . . . . . . . 10
term ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) |
15 | | ke 7 |
. . . . . . . . . 10
term ![=](eq.gif) |
16 | 12, 14, 15 | kbr 9 |
. . . . . . . . 9
term ![[](lbrack.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![]](rbrack.gif) |
17 | 11, 13, 15 | kbr 9 |
. . . . . . . . 9
term ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) |
18 | | tim 121 |
. . . . . . . . 9
term ![==>](bigto.gif) |
19 | 16, 17, 18 | kbr 9 |
. . . . . . . 8
term ![[](lbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif)
![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![]](rbrack.gif) |
20 | 3, 9, 19 | kl 6 |
. . . . . . 7
term ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif)
![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![]](rbrack.gif) |
21 | 7, 20 | kc 5 |
. . . . . 6
term ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif)
![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![]](rbrack.gif) ![)](rp.gif) |
22 | 3, 8, 21 | kl 6 |
. . . . 5
term ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) ![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![]](rbrack.gif) ![)](rp.gif) |
23 | 7, 22 | kc 5 |
. . . 4
term ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif)
![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![]](rbrack.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 5, 6, 23 | kl 6 |
. . 3
term ![\](lambda.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif)
![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![]](rbrack.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 2, 24, 15 | kbr 9 |
. 2
term 1-1
![\](lambda.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif)
![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![]](rbrack.gif) ![)](rp.gif) ![)](rp.gif) ![]](rbrack.gif) |
26 | 1, 25 | wffMMJ2 11 |
1
wff 1-1 ![\](lambda.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![y](_y.gif) ![:](colon.gif) ![[](lbrack.gif) ![[](lbrack.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![(](lp.gif) ![f](_f.gif) ![:](colon.gif) ![(](lp.gif) ![be](_beta.gif) ![)](rp.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif)
![[](lbrack.gif) ![x](_x.gif) ![:](colon.gif) ![y](_y.gif) ![:](colon.gif) ![al](_alpha.gif) ![]](rbrack.gif) ![]](rbrack.gif) ![)](rp.gif) ![)](rp.gif) ![]](rbrack.gif) |