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		snex	⊢ { 𝑥 } ∈ 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 )