# 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 ${⊢}\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\to {A}\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\wedge {A}=\varnothing \right)\to {A}=\varnothing$
2 0ex ${⊢}\varnothing \in \mathrm{V}$
3 1 2 eqeltrdi ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\wedge {A}=\varnothing \right)\to {A}\in \mathrm{V}$
4 n0 ${⊢}{A}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
5 snex ${⊢}\left\{{x}\right\}\in \mathrm{V}$
6 dmexg ${⊢}{R}\in {V}\to \mathrm{dom}{R}\in \mathrm{V}$
7 rnexg ${⊢}{R}\in {V}\to \mathrm{ran}{R}\in \mathrm{V}$
8 unexg ${⊢}\left(\mathrm{dom}{R}\in \mathrm{V}\wedge \mathrm{ran}{R}\in \mathrm{V}\right)\to \mathrm{dom}{R}\cup \mathrm{ran}{R}\in \mathrm{V}$
9 6 7 8 syl2anc ${⊢}{R}\in {V}\to \mathrm{dom}{R}\cup \mathrm{ran}{R}\in \mathrm{V}$
10 unexg ${⊢}\left(\left\{{x}\right\}\in \mathrm{V}\wedge \mathrm{dom}{R}\cup \mathrm{ran}{R}\in \mathrm{V}\right)\to \left\{{x}\right\}\cup \left(\mathrm{dom}{R}\cup \mathrm{ran}{R}\right)\in \mathrm{V}$
11 5 9 10 sylancr ${⊢}{R}\in {V}\to \left\{{x}\right\}\cup \left(\mathrm{dom}{R}\cup \mathrm{ran}{R}\right)\in \mathrm{V}$
12 11 ad2antlr ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\wedge {x}\in {A}\right)\to \left\{{x}\right\}\cup \left(\mathrm{dom}{R}\cup \mathrm{ran}{R}\right)\in \mathrm{V}$
13 sossfld ${⊢}\left({R}\mathrm{Or}{A}\wedge {x}\in {A}\right)\to {A}\setminus \left\{{x}\right\}\subseteq \mathrm{dom}{R}\cup \mathrm{ran}{R}$
14 13 adantlr ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\wedge {x}\in {A}\right)\to {A}\setminus \left\{{x}\right\}\subseteq \mathrm{dom}{R}\cup \mathrm{ran}{R}$
15 ssundif ${⊢}{A}\subseteq \left\{{x}\right\}\cup \left(\mathrm{dom}{R}\cup \mathrm{ran}{R}\right)↔{A}\setminus \left\{{x}\right\}\subseteq \mathrm{dom}{R}\cup \mathrm{ran}{R}$
16 14 15 sylibr ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\wedge {x}\in {A}\right)\to {A}\subseteq \left\{{x}\right\}\cup \left(\mathrm{dom}{R}\cup \mathrm{ran}{R}\right)$
17 12 16 ssexd ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\wedge {x}\in {A}\right)\to {A}\in \mathrm{V}$
18 17 ex ${⊢}\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\to \left({x}\in {A}\to {A}\in \mathrm{V}\right)$
19 18 exlimdv ${⊢}\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}\to {A}\in \mathrm{V}\right)$
20 19 imp ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}\right)\to {A}\in \mathrm{V}$
21 4 20 sylan2b ${⊢}\left(\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\wedge {A}\ne \varnothing \right)\to {A}\in \mathrm{V}$
22 3 21 pm2.61dane ${⊢}\left({R}\mathrm{Or}{A}\wedge {R}\in {V}\right)\to {A}\in \mathrm{V}$