This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) → 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) ∧ 𝐴 = ∅ ) → 𝐴 = ∅ )
2 0ex ⊢ ∅ ∈ V
3 1 2 eqeltrdi ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) ∧ 𝐴 = ∅ ) → 𝐴 ∈ V )
4 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
5 vsnex ⊢ { 𝑥 } ∈ V
6 dmexg ⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
7 rnexg ⊢ ( 𝑅 ∈ 𝑉 → ran 𝑅 ∈ V )
8 unexg ⊢ ( ( dom 𝑅 ∈ V ∧ ran 𝑅 ∈ V ) → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
9 6 7 8 syl2anc ⊢ ( 𝑅 ∈ 𝑉 → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
10 unexg ⊢ ( ( { 𝑥 } ∈ V ∧ ( dom 𝑅 ∪ ran 𝑅 ) ∈ V ) → ( { 𝑥 } ∪ ( dom 𝑅 ∪ ran 𝑅 ) ) ∈ V )
11 5 9 10 sylancr ⊢ ( 𝑅 ∈ 𝑉 → ( { 𝑥 } ∪ ( dom 𝑅 ∪ ran 𝑅 ) ) ∈ V )
12 11 ad2antlr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐴 ) → ( { 𝑥 } ∪ ( dom 𝑅 ∪ ran 𝑅 ) ) ∈ V )
13 sossfld ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
14 13 adantlr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
15 ssundif ⊢ ( 𝐴 ⊆ ( { 𝑥 } ∪ ( dom 𝑅 ∪ ran 𝑅 ) ) ↔ ( 𝐴 ∖ { 𝑥 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
16 14 15 sylibr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ ( { 𝑥 } ∪ ( dom 𝑅 ∪ ran 𝑅 ) ) )
17 12 16 ssexd ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ V )
18 17 ex ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐴 → 𝐴 ∈ V ) )
19 18 exlimdv ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) → ( ∃ 𝑥 𝑥 ∈ 𝐴 → 𝐴 ∈ V ) )
20 19 imp ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) ∧ ∃ 𝑥 𝑥 ∈ 𝐴 ) → 𝐴 ∈ V )
21 4 20 sylan2b ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ V )
22 3 21 pm2.61dane ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) → 𝐴 ∈ V )