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 vsnex ⊢ 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