Metamath Proof Explorer

Theorem soex

Description: If the relation in a strict order is a set, then the base field is also a set. (Contributed by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion soex 
|- ( ( R Or A /\ R e. V ) -> A e. _V )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( R Or A /\ R e. V ) /\ A = (/) ) -> A = (/) )
2 0ex 
 |-  (/) e. _V
3 1 2 eqeltrdi 
 |-  ( ( ( R Or A /\ R e. V ) /\ A = (/) ) -> A e. _V )
4 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
5 snex 
 |-  { x } e. _V
6 dmexg 
 |-  ( R e. V -> dom R e. _V )
7 rnexg 
 |-  ( R e. V -> ran R e. _V )
8 unexg 
 |-  ( ( dom R e. _V /\ ran R e. _V ) -> ( dom R u. ran R ) e. _V )
9 6 7 8 syl2anc 
 |-  ( R e. V -> ( dom R u. ran R ) e. _V )
10 unexg 
 |-  ( ( { x } e. _V /\ ( dom R u. ran R ) e. _V ) -> ( { x } u. ( dom R u. ran R ) ) e. _V )
11 5 9 10 sylancr 
 |-  ( R e. V -> ( { x } u. ( dom R u. ran R ) ) e. _V )
12 11 ad2antlr 
 |-  ( ( ( R Or A /\ R e. V ) /\ x e. A ) -> ( { x } u. ( dom R u. ran R ) ) e. _V )
13 sossfld 
 |-  ( ( R Or A /\ x e. A ) -> ( A \ { x } ) C_ ( dom R u. ran R ) )
14 13 adantlr 
 |-  ( ( ( R Or A /\ R e. V ) /\ x e. A ) -> ( A \ { x } ) C_ ( dom R u. ran R ) )
15 ssundif 
 |-  ( A C_ ( { x } u. ( dom R u. ran R ) ) <-> ( A \ { x } ) C_ ( dom R u. ran R ) )
16 14 15 sylibr 
 |-  ( ( ( R Or A /\ R e. V ) /\ x e. A ) -> A C_ ( { x } u. ( dom R u. ran R ) ) )
17 12 16 ssexd 
 |-  ( ( ( R Or A /\ R e. V ) /\ x e. A ) -> A e. _V )
18 17 ex 
 |-  ( ( R Or A /\ R e. V ) -> ( x e. A -> A e. _V ) )
19 18 exlimdv 
 |-  ( ( R Or A /\ R e. V ) -> ( E. x x e. A -> A e. _V ) )
20 19 imp 
 |-  ( ( ( R Or A /\ R e. V ) /\ E. x x e. A ) -> A e. _V )
21 4 20 sylan2b 
 |-  ( ( ( R Or A /\ R e. V ) /\ A =/= (/) ) -> A e. _V )
22 3 21 pm2.61dane 
 |-  ( ( R Or A /\ R e. V ) -> A e. _V )