Description: Each ordinal that is comparable with an element of the universe is in the universe. (Contributed by Mario Carneiro, 10-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | grudomon | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 | |
|
2 | eleq1 | |
|
3 | 1 2 | imbi12d | |
4 | 3 | imbi2d | |
5 | breq1 | |
|
6 | eleq1 | |
|
7 | 5 6 | imbi12d | |
8 | 7 | imbi2d | |
9 | r19.21v | |
|
10 | simpl1 | |
|
11 | vex | |
|
12 | onelss | |
|
13 | 12 | imp | |
14 | ssdomg | |
|
15 | 11 13 14 | mpsyl | |
16 | 10 15 | sylan | |
17 | simplr | |
|
18 | domtr | |
|
19 | 16 17 18 | syl2anc | |
20 | pm2.27 | |
|
21 | 19 20 | syl | |
22 | 21 | ralimdva | |
23 | dfss3 | |
|
24 | domeng | |
|
25 | 24 | 3ad2ant3 | |
26 | 25 | biimpa | |
27 | simpl2 | |
|
28 | gruss | |
|
29 | 28 | 3expia | |
30 | 29 | 3adant1 | |
31 | 30 | adantr | |
32 | ensym | |
|
33 | 31 32 | anim12d1 | |
34 | 33 | ancomsd | |
35 | 34 | eximdv | |
36 | gruen | |
|
37 | 36 | 3com23 | |
38 | 37 | 3exp | |
39 | 38 | exlimdv | |
40 | 27 35 39 | sylsyld | |
41 | 26 40 | mpd | |
42 | 23 41 | syl5bir | |
43 | 22 42 | syld | |
44 | 43 | ex | |
45 | 44 | com23 | |
46 | 45 | 3expib | |
47 | 46 | a2d | |
48 | 9 47 | syl5bi | |
49 | 4 8 48 | tfis3 | |
50 | 49 | com3l | |
51 | 50 | impr | |
52 | 51 | 3impia | |
53 | 52 | 3com23 | |