sofld

Description: The base set of a nonempty strict order is the same as the field of the relation. (Contributed by Mario Carneiro, 15-May-2015)

		Ref	Expression
	Assertion	sofld	$⊢ (R Or A \land R \subseteq A \times A \land R \neq \emptyset) \to A = dom R \cup ran R$

Proof

Step	Hyp	Ref	Expression
1		relxp	$⊢ Rel (A \times A)$
2		relss	$⊢ R \subseteq A \times A \to (Rel (A \times A) \to Rel R)$
3	1 2	mpi	$⊢ R \subseteq A \times A \to Rel R$
4	3	ad2antlr	$⊢ ((R Or A \land R \subseteq A \times A) \land \neg A \subseteq dom R \cup ran R) \to Rel R$
5		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
6		ssun1	$⊢ A \subseteq A \cup \{x\}$
7		undif1	$⊢ (A ∖ \{x\}) \cup \{x\} = A \cup \{x\}$
8	6 7	sseqtrri	$⊢ A \subseteq (A ∖ \{x\}) \cup \{x\}$
9		simpll	$⊢ ((R Or A \land R \subseteq A \times A) \land x R y) \to R Or A$
10		dmss	$⊢ R \subseteq A \times A \to dom R \subseteq dom (A \times A)$
11		dmxpid	$⊢ dom (A \times A) = A$
12	10 11	sseqtrdi	$⊢ R \subseteq A \times A \to dom R \subseteq A$
13	12	ad2antlr	$⊢ ((R Or A \land R \subseteq A \times A) \land x R y) \to dom R \subseteq A$
14	3	ad2antlr	$⊢ ((R Or A \land R \subseteq A \times A) \land x R y) \to Rel R$
15		releldm	$⊢ (Rel R \land x R y) \to x \in dom R$
16	14 15	sylancom	$⊢ ((R Or A \land R \subseteq A \times A) \land x R y) \to x \in dom R$
17	13 16	sseldd	$⊢ ((R Or A \land R \subseteq A \times A) \land x R y) \to x \in A$
18		sossfld	$⊢ (R Or A \land x \in A) \to A ∖ \{x\} \subseteq dom R \cup ran R$
19	9 17 18	syl2anc	$⊢ ((R Or A \land R \subseteq A \times A) \land x R y) \to A ∖ \{x\} \subseteq dom R \cup ran R$
20		ssun1	$⊢ dom R \subseteq dom R \cup ran R$
21	20 16	sselid	$⊢ ((R Or A \land R \subseteq A \times A) \land x R y) \to x \in (dom R \cup ran R)$
22	21	snssd	$⊢ ((R Or A \land R \subseteq A \times A) \land x R y) \to \{x\} \subseteq dom R \cup ran R$
23	19 22	unssd	$⊢ ((R Or A \land R \subseteq A \times A) \land x R y) \to (A ∖ \{x\}) \cup \{x\} \subseteq dom R \cup ran R$
24	8 23	sstrid	$⊢ ((R Or A \land R \subseteq A \times A) \land x R y) \to A \subseteq dom R \cup ran R$
25	24	ex	$⊢ (R Or A \land R \subseteq A \times A) \to (x R y \to A \subseteq dom R \cup ran R)$
26	5 25	biimtrrid	$⊢ (R Or A \land R \subseteq A \times A) \to (⟨x, y⟩ \in R \to A \subseteq dom R \cup ran R)$
27	26	con3dimp	$⊢ ((R Or A \land R \subseteq A \times A) \land \neg A \subseteq dom R \cup ran R) \to \neg ⟨x, y⟩ \in R$
28	27	pm2.21d	$⊢ ((R Or A \land R \subseteq A \times A) \land \neg A \subseteq dom R \cup ran R) \to (⟨x, y⟩ \in R \to ⟨x, y⟩ \in \emptyset)$
29	4 28	relssdv	$⊢ ((R Or A \land R \subseteq A \times A) \land \neg A \subseteq dom R \cup ran R) \to R \subseteq \emptyset$
30		ss0	$⊢ R \subseteq \emptyset \to R = \emptyset$
31	29 30	syl	$⊢ ((R Or A \land R \subseteq A \times A) \land \neg A \subseteq dom R \cup ran R) \to R = \emptyset$
32	31	ex	$⊢ (R Or A \land R \subseteq A \times A) \to (\neg A \subseteq dom R \cup ran R \to R = \emptyset)$
33	32	necon1ad	$⊢ (R Or A \land R \subseteq A \times A) \to (R \neq \emptyset \to A \subseteq dom R \cup ran R)$
34	33	3impia	$⊢ (R Or A \land R \subseteq A \times A \land R \neq \emptyset) \to A \subseteq dom R \cup ran R$
35		rnss	$⊢ R \subseteq A \times A \to ran R \subseteq ran (A \times A)$
36		rnxpid	$⊢ ran (A \times A) = A$
37	35 36	sseqtrdi	$⊢ R \subseteq A \times A \to ran R \subseteq A$
38	12 37	unssd	$⊢ R \subseteq A \times A \to dom R \cup ran R \subseteq A$
39	38	3ad2ant2	$⊢ (R Or A \land R \subseteq A \times A \land R \neq \emptyset) \to dom R \cup ran R \subseteq A$
40	34 39	eqssd	$⊢ (R Or A \land R \subseteq A \times A \land R \neq \emptyset) \to A = dom R \cup ran R$

Metamath Proof Explorer

Theorem sofld

Proof