Metamath Proof Explorer


Theorem grudomon

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 UUnivAOnBUABAU

Proof

Step Hyp Ref Expression
1 breq1 x=yxByB
2 eleq1 x=yxUyU
3 1 2 imbi12d x=yxBxUyByU
4 3 imbi2d x=yUUnivBUxBxUUUnivBUyByU
5 breq1 x=AxBAB
6 eleq1 x=AxUAU
7 5 6 imbi12d x=AxBxUABAU
8 7 imbi2d x=AUUnivBUxBxUUUnivBUABAU
9 r19.21v yxUUnivBUyByUUUnivBUyxyByU
10 simpl1 xOnUUnivBUxBxOn
11 vex xV
12 onelss xOnyxyx
13 12 imp xOnyxyx
14 ssdomg xVyxyx
15 11 13 14 mpsyl xOnyxyx
16 10 15 sylan xOnUUnivBUxByxyx
17 simplr xOnUUnivBUxByxxB
18 domtr yxxByB
19 16 17 18 syl2anc xOnUUnivBUxByxyB
20 pm2.27 yByByUyU
21 19 20 syl xOnUUnivBUxByxyByUyU
22 21 ralimdva xOnUUnivBUxByxyByUyxyU
23 dfss3 xUyxyU
24 domeng BUxByxyyB
25 24 3ad2ant3 xOnUUnivBUxByxyyB
26 25 biimpa xOnUUnivBUxByxyyB
27 simpl2 xOnUUnivBUxBUUniv
28 gruss UUnivBUyByU
29 28 3expia UUnivBUyByU
30 29 3adant1 xOnUUnivBUyByU
31 30 adantr xOnUUnivBUxByByU
32 ensym xyyx
33 31 32 anim12d1 xOnUUnivBUxByBxyyUyx
34 33 ancomsd xOnUUnivBUxBxyyByUyx
35 34 eximdv xOnUUnivBUxByxyyByyUyx
36 gruen UUnivxUyUyxxU
37 36 3com23 UUnivyUyxxUxU
38 37 3exp UUnivyUyxxUxU
39 38 exlimdv UUnivyyUyxxUxU
40 27 35 39 sylsyld xOnUUnivBUxByxyyBxUxU
41 26 40 mpd xOnUUnivBUxBxUxU
42 23 41 syl5bir xOnUUnivBUxByxyUxU
43 22 42 syld xOnUUnivBUxByxyByUxU
44 43 ex xOnUUnivBUxByxyByUxU
45 44 com23 xOnUUnivBUyxyByUxBxU
46 45 3expib xOnUUnivBUyxyByUxBxU
47 46 a2d xOnUUnivBUyxyByUUUnivBUxBxU
48 9 47 syl5bi xOnyxUUnivBUyByUUUnivBUxBxU
49 4 8 48 tfis3 AOnUUnivBUABAU
50 49 com3l UUnivBUABAOnAU
51 50 impr UUnivBUABAOnAU
52 51 3impia UUnivBUABAOnAU
53 52 3com23 UUnivAOnBUABAU