Step | Hyp | Ref | Expression |
1 |
|
anllr |
A C_ B /\ isfun B /\ a, b e. A /\ a, c e. A -> isfun B |
2 |
|
an3l |
A C_ B /\ isfun B /\ a, b e. A /\ a, c e. A -> A C_ B |
3 |
|
anlr |
A C_ B /\ isfun B /\ a, b e. A /\ a, c e. A -> a, b e. A |
4 |
2, 3 |
sseld |
A C_ B /\ isfun B /\ a, b e. A /\ a, c e. A -> a, b e. B |
5 |
|
anr |
A C_ B /\ isfun B /\ a, b e. A /\ a, c e. A -> a, c e. A |
6 |
2, 5 |
sseld |
A C_ B /\ isfun B /\ a, b e. A /\ a, c e. A -> a, c e. B |
7 |
1, 4, 6 |
isfd |
A C_ B /\ isfun B /\ a, b e. A /\ a, c e. A -> b = c |
8 |
7 |
exp |
A C_ B /\ isfun B /\ a, b e. A -> a, c e. A -> b = c |
9 |
8 |
exp |
A C_ B /\ isfun B -> a, b e. A -> a, c e. A -> b = c |
10 |
9 |
iald |
A C_ B /\ isfun B -> A. c (a, b e. A -> a, c e. A -> b = c) |
11 |
10 |
iald |
A C_ B /\ isfun B -> A. b A. c (a, b e. A -> a, c e. A -> b = c) |
12 |
11 |
iald |
A C_ B /\ isfun B -> A. a A. b A. c (a, b e. A -> a, c e. A -> b = c) |
13 |
12 |
conv isfun |
A C_ B /\ isfun B -> isfun A |
14 |
13 |
exp |
A C_ B -> isfun B -> isfun A |