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 V A V

Proof

Step Hyp Ref Expression
1 simpr R Or A R V A = A =
2 0ex V
3 1 2 eqeltrdi R Or A R V A = A V
4 n0 A x x A
5 snex x V
6 dmexg R V dom R V
7 rnexg R V ran R V
8 unexg dom R V ran R V dom R ran R V
9 6 7 8 syl2anc R V dom R ran R V
10 unexg x V dom R ran R V x dom R ran R V
11 5 9 10 sylancr R V x dom R ran R V
12 11 ad2antlr R Or A R V x A x dom R ran R V
13 sossfld R Or A x A A x dom R ran R
14 13 adantlr R Or A R V x A A x dom R ran R
15 ssundif A x dom R ran R A x dom R ran R
16 14 15 sylibr R Or A R V x A A x dom R ran R
17 12 16 ssexd R Or A R V x A A V
18 17 ex R Or A R V x A A V
19 18 exlimdv R Or A R V x x A A V
20 19 imp R Or A R V x x A A V
21 4 20 sylan2b R Or A R V A A V
22 3 21 pm2.61dane R Or A R V A V