Description: Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isinitoi.b | |
|
isinitoi.h | |
||
isinitoi.c | |
||
Assertion | isinitoi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isinitoi.b | |
|
2 | isinitoi.h | |
|
3 | isinitoi.c | |
|
4 | 3 1 2 | initoval | |
5 | 4 | eleq2d | |
6 | elrabi | |
|
7 | 5 6 | syl6bi | |
8 | 7 | imp | |
9 | 3 | adantr | |
10 | simpr | |
|
11 | 1 2 9 10 | isinito | |
12 | 11 | biimpd | |
13 | 12 | impancom | |
14 | 8 13 | jcai | |