Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | onfrALTlem3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid | |
|
2 | simpr | |
|
3 | 2 | a1i | |
4 | df-ne | |
|
5 | 3 4 | syl6ibr | |
6 | pm3.2 | |
|
7 | 1 5 6 | mpsylsyld | |
8 | vex | |
|
9 | 8 | inex2 | |
10 | inss2 | |
|
11 | simpl | |
|
12 | simpl | |
|
13 | ssel | |
|
14 | 11 12 13 | syl2im | |
15 | eloni | |
|
16 | 14 15 | syl6 | |
17 | ordwe | |
|
18 | 16 17 | syl6 | |
19 | wess | |
|
20 | 10 18 19 | mpsylsyld | |
21 | wefr | |
|
22 | 20 21 | syl6 | |
23 | dfepfr | |
|
24 | 22 23 | imbitrdi | |
25 | spsbc | |
|
26 | 9 24 25 | mpsylsyld | |
27 | onfrALTlem5 | |
|
28 | 26 27 | imbitrdi | |
29 | 7 28 | mpdd | |