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 
|- ( ( U e. Univ /\ A e. On /\ ( B e. U /\ A ~<_ B ) ) -> A e. U )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = y -> ( x ~<_ B <-> y ~<_ B ) )
2 eleq1 
 |-  ( x = y -> ( x e. U <-> y e. U ) )
3 1 2 imbi12d 
 |-  ( x = y -> ( ( x ~<_ B -> x e. U ) <-> ( y ~<_ B -> y e. U ) ) )
4 3 imbi2d 
 |-  ( x = y -> ( ( ( U e. Univ /\ B e. U ) -> ( x ~<_ B -> x e. U ) ) <-> ( ( U e. Univ /\ B e. U ) -> ( y ~<_ B -> y e. U ) ) ) )
5 breq1 
 |-  ( x = A -> ( x ~<_ B <-> A ~<_ B ) )
6 eleq1 
 |-  ( x = A -> ( x e. U <-> A e. U ) )
7 5 6 imbi12d 
 |-  ( x = A -> ( ( x ~<_ B -> x e. U ) <-> ( A ~<_ B -> A e. U ) ) )
8 7 imbi2d 
 |-  ( x = A -> ( ( ( U e. Univ /\ B e. U ) -> ( x ~<_ B -> x e. U ) ) <-> ( ( U e. Univ /\ B e. U ) -> ( A ~<_ B -> A e. U ) ) ) )
9 r19.21v 
 |-  ( A. y e. x ( ( U e. Univ /\ B e. U ) -> ( y ~<_ B -> y e. U ) ) <-> ( ( U e. Univ /\ B e. U ) -> A. y e. x ( y ~<_ B -> y e. U ) ) )
10 simpl1 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> x e. On )
11 vex 
 |-  x e. _V
12 onelss 
 |-  ( x e. On -> ( y e. x -> y C_ x ) )
13 12 imp 
 |-  ( ( x e. On /\ y e. x ) -> y C_ x )
14 ssdomg 
 |-  ( x e. _V -> ( y C_ x -> y ~<_ x ) )
15 11 13 14 mpsyl 
 |-  ( ( x e. On /\ y e. x ) -> y ~<_ x )
16 10 15 sylan 
 |-  ( ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) /\ y e. x ) -> y ~<_ x )
17 simplr 
 |-  ( ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) /\ y e. x ) -> x ~<_ B )
18 domtr 
 |-  ( ( y ~<_ x /\ x ~<_ B ) -> y ~<_ B )
19 16 17 18 syl2anc 
 |-  ( ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) /\ y e. x ) -> y ~<_ B )
20 pm2.27 
 |-  ( y ~<_ B -> ( ( y ~<_ B -> y e. U ) -> y e. U ) )
21 19 20 syl 
 |-  ( ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) /\ y e. x ) -> ( ( y ~<_ B -> y e. U ) -> y e. U ) )
22 21 ralimdva 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> ( A. y e. x ( y ~<_ B -> y e. U ) -> A. y e. x y e. U ) )
23 dfss3 
 |-  ( x C_ U <-> A. y e. x y e. U )
24 domeng 
 |-  ( B e. U -> ( x ~<_ B <-> E. y ( x ~~ y /\ y C_ B ) ) )
25 24 3ad2ant3 
 |-  ( ( x e. On /\ U e. Univ /\ B e. U ) -> ( x ~<_ B <-> E. y ( x ~~ y /\ y C_ B ) ) )
26 25 biimpa 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> E. y ( x ~~ y /\ y C_ B ) )
27 simpl2 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> U e. Univ )
28 gruss 
 |-  ( ( U e. Univ /\ B e. U /\ y C_ B ) -> y e. U )
29 28 3expia 
 |-  ( ( U e. Univ /\ B e. U ) -> ( y C_ B -> y e. U ) )
30 29 3adant1 
 |-  ( ( x e. On /\ U e. Univ /\ B e. U ) -> ( y C_ B -> y e. U ) )
31 30 adantr 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> ( y C_ B -> y e. U ) )
32 ensym 
 |-  ( x ~~ y -> y ~~ x )
33 31 32 anim12d1 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> ( ( y C_ B /\ x ~~ y ) -> ( y e. U /\ y ~~ x ) ) )
34 33 ancomsd 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> ( ( x ~~ y /\ y C_ B ) -> ( y e. U /\ y ~~ x ) ) )
35 34 eximdv 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> ( E. y ( x ~~ y /\ y C_ B ) -> E. y ( y e. U /\ y ~~ x ) ) )
36 gruen 
 |-  ( ( U e. Univ /\ x C_ U /\ ( y e. U /\ y ~~ x ) ) -> x e. U )
37 36 3com23 
 |-  ( ( U e. Univ /\ ( y e. U /\ y ~~ x ) /\ x C_ U ) -> x e. U )
38 37 3exp 
 |-  ( U e. Univ -> ( ( y e. U /\ y ~~ x ) -> ( x C_ U -> x e. U ) ) )
39 38 exlimdv 
 |-  ( U e. Univ -> ( E. y ( y e. U /\ y ~~ x ) -> ( x C_ U -> x e. U ) ) )
40 27 35 39 sylsyld 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> ( E. y ( x ~~ y /\ y C_ B ) -> ( x C_ U -> x e. U ) ) )
41 26 40 mpd 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> ( x C_ U -> x e. U ) )
42 23 41 syl5bir 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> ( A. y e. x y e. U -> x e. U ) )
43 22 42 syld 
 |-  ( ( ( x e. On /\ U e. Univ /\ B e. U ) /\ x ~<_ B ) -> ( A. y e. x ( y ~<_ B -> y e. U ) -> x e. U ) )
44 43 ex 
 |-  ( ( x e. On /\ U e. Univ /\ B e. U ) -> ( x ~<_ B -> ( A. y e. x ( y ~<_ B -> y e. U ) -> x e. U ) ) )
45 44 com23 
 |-  ( ( x e. On /\ U e. Univ /\ B e. U ) -> ( A. y e. x ( y ~<_ B -> y e. U ) -> ( x ~<_ B -> x e. U ) ) )
46 45 3expib 
 |-  ( x e. On -> ( ( U e. Univ /\ B e. U ) -> ( A. y e. x ( y ~<_ B -> y e. U ) -> ( x ~<_ B -> x e. U ) ) ) )
47 46 a2d 
 |-  ( x e. On -> ( ( ( U e. Univ /\ B e. U ) -> A. y e. x ( y ~<_ B -> y e. U ) ) -> ( ( U e. Univ /\ B e. U ) -> ( x ~<_ B -> x e. U ) ) ) )
48 9 47 syl5bi 
 |-  ( x e. On -> ( A. y e. x ( ( U e. Univ /\ B e. U ) -> ( y ~<_ B -> y e. U ) ) -> ( ( U e. Univ /\ B e. U ) -> ( x ~<_ B -> x e. U ) ) ) )
49 4 8 48 tfis3 
 |-  ( A e. On -> ( ( U e. Univ /\ B e. U ) -> ( A ~<_ B -> A e. U ) ) )
50 49 com3l 
 |-  ( ( U e. Univ /\ B e. U ) -> ( A ~<_ B -> ( A e. On -> A e. U ) ) )
51 50 impr 
 |-  ( ( U e. Univ /\ ( B e. U /\ A ~<_ B ) ) -> ( A e. On -> A e. U ) )
52 51 3impia 
 |-  ( ( U e. Univ /\ ( B e. U /\ A ~<_ B ) /\ A e. On ) -> A e. U )
53 52 3com23 
 |-  ( ( U e. Univ /\ A e. On /\ ( B e. U /\ A ~<_ B ) ) -> A e. U )