trclublem

Description: If a relation exists then the class of transitive relations which are supersets of that relation is not empty. (Contributed by RP, 28-Apr-2020)

		Ref	Expression
	Assertion	trclublem	$⊢ R \in V \to R \cup (dom R \times ran R) \in \{x \| (R \subseteq x \land x \circ x \subseteq x)\}$

Proof

Step	Hyp	Ref	Expression
1		trclexlem	$⊢ R \in V \to R \cup (dom R \times ran R) \in V$
2		ssun1	$⊢ R \subseteq R \cup (dom R \times ran R)$
3		relcnv	$⊢ Rel R^{-1}$
4		relssdmrn	$⊢ Rel R^{-1} \to R^{-1} \subseteq dom R^{-1} \times ran R^{-1}$
5	3 4	ax-mp	$⊢ R^{-1} \subseteq dom R^{-1} \times ran R^{-1}$
6		ssequn1	$⊢ R^{-1} \subseteq dom R^{-1} \times ran R^{-1} \leftrightarrow R^{-1} \cup (dom R^{-1} \times ran R^{-1}) = dom R^{-1} \times ran R^{-1}$
7	5 6	mpbi	$⊢ R^{-1} \cup (dom R^{-1} \times ran R^{-1}) = dom R^{-1} \times ran R^{-1}$
8		cnvun	$⊢ {(R \cup (dom R \times ran R))}^{-1} = R^{-1} \cup {(dom R \times ran R)}^{-1}$
9		cnvxp	$⊢ {(dom R \times ran R)}^{-1} = ran R \times dom R$
10		df-rn	$⊢ ran R = dom R^{-1}$
11		dfdm4	$⊢ dom R = ran R^{-1}$
12	10 11	xpeq12i	$⊢ ran R \times dom R = dom R^{-1} \times ran R^{-1}$
13	9 12	eqtri	$⊢ {(dom R \times ran R)}^{-1} = dom R^{-1} \times ran R^{-1}$
14	13	uneq2i	$⊢ R^{-1} \cup {(dom R \times ran R)}^{-1} = R^{-1} \cup (dom R^{-1} \times ran R^{-1})$
15	8 14	eqtri	$⊢ {(R \cup (dom R \times ran R))}^{-1} = R^{-1} \cup (dom R^{-1} \times ran R^{-1})$
16	7 15 13	3eqtr4i	$⊢ {(R \cup (dom R \times ran R))}^{-1} = {(dom R \times ran R)}^{-1}$
17	16	breqi	$⊢ b {(R \cup (dom R \times ran R))}^{-1} a \leftrightarrow b {(dom R \times ran R)}^{-1} a$
18		vex	$⊢ b \in V$
19		vex	$⊢ a \in V$
20	18 19	brcnv	$⊢ b {(R \cup (dom R \times ran R))}^{-1} a \leftrightarrow a (R \cup (dom R \times ran R)) b$
21	18 19	brcnv	$⊢ b {(dom R \times ran R)}^{-1} a \leftrightarrow a (dom R \times ran R) b$
22	17 20 21	3bitr3i	$⊢ a (R \cup (dom R \times ran R)) b \leftrightarrow a (dom R \times ran R) b$
23	16	breqi	$⊢ c {(R \cup (dom R \times ran R))}^{-1} b \leftrightarrow c {(dom R \times ran R)}^{-1} b$
24		vex	$⊢ c \in V$
25	24 18	brcnv	$⊢ c {(R \cup (dom R \times ran R))}^{-1} b \leftrightarrow b (R \cup (dom R \times ran R)) c$
26	24 18	brcnv	$⊢ c {(dom R \times ran R)}^{-1} b \leftrightarrow b (dom R \times ran R) c$
27	23 25 26	3bitr3i	$⊢ b (R \cup (dom R \times ran R)) c \leftrightarrow b (dom R \times ran R) c$
28	22 27	anbi12i	$⊢ (a (R \cup (dom R \times ran R)) b \land b (R \cup (dom R \times ran R)) c) \leftrightarrow (a (dom R \times ran R) b \land b (dom R \times ran R) c)$
29	28	biimpi	$⊢ (a (R \cup (dom R \times ran R)) b \land b (R \cup (dom R \times ran R)) c) \to (a (dom R \times ran R) b \land b (dom R \times ran R) c)$
30	29	eximi	$⊢ \exists b (a (R \cup (dom R \times ran R)) b \land b (R \cup (dom R \times ran R)) c) \to \exists b (a (dom R \times ran R) b \land b (dom R \times ran R) c)$
31	30	ssopab2i	$⊢ \{⟨a, c⟩ \| \exists b (a (R \cup (dom R \times ran R)) b \land b (R \cup (dom R \times ran R)) c)\} \subseteq \{⟨a, c⟩ \| \exists b (a (dom R \times ran R) b \land b (dom R \times ran R) c)\}$
32		df-co	$⊢ (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) = \{⟨a, c⟩ \| \exists b (a (R \cup (dom R \times ran R)) b \land b (R \cup (dom R \times ran R)) c)\}$
33		df-co	$⊢ (dom R \times ran R) \circ (dom R \times ran R) = \{⟨a, c⟩ \| \exists b (a (dom R \times ran R) b \land b (dom R \times ran R) c)\}$
34	31 32 33	3sstr4i	$⊢ (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) \subseteq (dom R \times ran R) \circ (dom R \times ran R)$
35		xptrrel	$⊢ (dom R \times ran R) \circ (dom R \times ran R) \subseteq dom R \times ran R$
36		ssun2	$⊢ dom R \times ran R \subseteq R \cup (dom R \times ran R)$
37	35 36	sstri	$⊢ (dom R \times ran R) \circ (dom R \times ran R) \subseteq R \cup (dom R \times ran R)$
38	34 37	sstri	$⊢ (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) \subseteq R \cup (dom R \times ran R)$
39		trcleq2lem	$⊢ x = R \cup (dom R \times ran R) \to ((R \subseteq x \land x \circ x \subseteq x) \leftrightarrow (R \subseteq R \cup (dom R \times ran R) \land (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) \subseteq R \cup (dom R \times ran R)))$
40	39	elabg	$⊢ R \cup (dom R \times ran R) \in V \to (R \cup (dom R \times ran R) \in \{x \| (R \subseteq x \land x \circ x \subseteq x)\} \leftrightarrow (R \subseteq R \cup (dom R \times ran R) \land (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) \subseteq R \cup (dom R \times ran R)))$
41	40	biimprd	$⊢ R \cup (dom R \times ran R) \in V \to ((R \subseteq R \cup (dom R \times ran R) \land (R \cup (dom R \times ran R)) \circ (R \cup (dom R \times ran R)) \subseteq R \cup (dom R \times ran R)) \to R \cup (dom R \times ran R) \in \{x \| (R \subseteq x \land x \circ x \subseteq x)\})$
42	2 38 41	mp2ani	$⊢ R \cup (dom R \times ran R) \in V \to R \cup (dom R \times ran R) \in \{x \| (R \subseteq x \land x \circ x \subseteq x)\}$
43	1 42	syl	$⊢ R \in V \to R \cup (dom R \times ran R) \in \{x \| (R \subseteq x \land x \circ x \subseteq x)\}$

Metamath Proof Explorer

Theorem trclublem

Proof