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 \land R \in V) \to A \in V$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((R Or A \land R \in V) \land A = \emptyset) \to A = \emptyset$
2		0ex	$⊢ \emptyset \in V$
3	1 2	eqeltrdi	$⊢ ((R Or A \land R \in V) \land A = \emptyset) \to A \in V$
4		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
5		vsnex	$⊢ \{x\} \in V$
6		dmexg	$⊢ R \in V \to dom R \in V$
7		rnexg	$⊢ R \in V \to ran R \in V$
8		unexg	$⊢ (dom R \in V \land ran R \in V) \to dom R \cup ran R \in V$
9	6 7 8	syl2anc	$⊢ R \in V \to dom R \cup ran R \in V$
10		unexg	$⊢ (\{x\} \in V \land dom R \cup ran R \in V) \to \{x\} \cup (dom R \cup ran R) \in V$
11	5 9 10	sylancr	$⊢ R \in V \to \{x\} \cup (dom R \cup ran R) \in V$
12	11	ad2antlr	$⊢ ((R Or A \land R \in V) \land x \in A) \to \{x\} \cup (dom R \cup ran R) \in V$
13		sossfld	$⊢ (R Or A \land x \in A) \to A ∖ \{x\} \subseteq dom R \cup ran R$
14	13	adantlr	$⊢ ((R Or A \land R \in V) \land x \in A) \to A ∖ \{x\} \subseteq dom R \cup ran R$
15		ssundif	$⊢ A \subseteq \{x\} \cup (dom R \cup ran R) \leftrightarrow A ∖ \{x\} \subseteq dom R \cup ran R$
16	14 15	sylibr	$⊢ ((R Or A \land R \in V) \land x \in A) \to A \subseteq \{x\} \cup (dom R \cup ran R)$
17	12 16	ssexd	$⊢ ((R Or A \land R \in V) \land x \in A) \to A \in V$
18	17	ex	$⊢ (R Or A \land R \in V) \to (x \in A \to A \in V)$
19	18	exlimdv	$⊢ (R Or A \land R \in V) \to (\exists x x \in A \to A \in V)$
20	19	imp	$⊢ ((R Or A \land R \in V) \land \exists x x \in A) \to A \in V$
21	4 20	sylan2b	$⊢ ((R Or A \land R \in V) \land A \neq \emptyset) \to A \in V$
22	3 21	pm2.61dane	$⊢ (R Or A \land R \in V) \to A \in V$

Metamath Proof Explorer

Theorem soex

Proof