brtrclfv2

Description: Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020)

		Ref	Expression
	Assertion	brtrclfv2	$⊢ (X \in U \land Y \in V \land R \in W) \to (X t+ (R) Y \leftrightarrow Y \in ⋂ \{f \| R [\{X\} \cup f] \subseteq f\})$

Proof

Step	Hyp	Ref	Expression
1		df-br	$⊢ X ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} Y \leftrightarrow ⟨X, Y⟩ \in ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
2	1	a1i	$⊢ (X \in U \land Y \in V \land R \in W) \to (X ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} Y \leftrightarrow ⟨X, Y⟩ \in ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\})$
3		trclfv	$⊢ R \in W \to t+ (R) = ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
4	3	breqd	$⊢ R \in W \to (X t+ (R) Y \leftrightarrow X ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} Y)$
5	4	3ad2ant3	$⊢ (X \in U \land Y \in V \land R \in W) \to (X t+ (R) Y \leftrightarrow X ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} Y)$
6		elimasng	$⊢ (X \in U \land Y \in V) \to (Y \in ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} [\{X\}] \leftrightarrow ⟨X, Y⟩ \in ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\})$
7	6	3adant3	$⊢ (X \in U \land Y \in V \land R \in W) \to (Y \in ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} [\{X\}] \leftrightarrow ⟨X, Y⟩ \in ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\})$
8	2 5 7	3bitr4d	$⊢ (X \in U \land Y \in V \land R \in W) \to (X t+ (R) Y \leftrightarrow Y \in ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} [\{X\}])$
9		intimasn	$⊢ X \in U \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} [\{X\}] = ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\}$
10	9	3ad2ant1	$⊢ (X \in U \land Y \in V \land R \in W) \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} [\{X\}] = ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\}$
11		simpl3	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to R \in W$
12		snex	$⊢ \{X\} \in V$
13		vex	$⊢ f \in V$
14	12 13	xpex	$⊢ \{X\} \times f \in V$
15		unexg	$⊢ (R \in W \land \{X\} \times f \in V) \to R \cup (\{X\} \times f) \in V$
16	11 14 15	sylancl	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to R \cup (\{X\} \times f) \in V$
17		trclfvlb	$⊢ R \cup (\{X\} \times f) \in V \to R \cup (\{X\} \times f) \subseteq t+ (R \cup (\{X\} \times f))$
18	17	unssad	$⊢ R \cup (\{X\} \times f) \in V \to R \subseteq t+ (R \cup (\{X\} \times f))$
19	16 18	syl	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to R \subseteq t+ (R \cup (\{X\} \times f))$
20		trclfvcotrg	$⊢ t+ (R \cup (\{X\} \times f)) \circ t+ (R \cup (\{X\} \times f)) \subseteq t+ (R \cup (\{X\} \times f))$
21	20	a1i	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to t+ (R \cup (\{X\} \times f)) \circ t+ (R \cup (\{X\} \times f)) \subseteq t+ (R \cup (\{X\} \times f))$
22		simpl1	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to X \in U$
23		snidg	$⊢ X \in U \to X \in \{X\}$
24	22 23	syl	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to X \in \{X\}$
25		inelcm	$⊢ (X \in \{X\} \land X \in \{X\}) \to \{X\} \cap \{X\} \neq \emptyset$
26	24 24 25	syl2anc	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to \{X\} \cap \{X\} \neq \emptyset$
27		xpima2	$⊢ \{X\} \cap \{X\} \neq \emptyset \to (\{X\} \times f) [\{X\}] = f$
28	26 27	syl	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to (\{X\} \times f) [\{X\}] = f$
29	16 17	syl	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to R \cup (\{X\} \times f) \subseteq t+ (R \cup (\{X\} \times f))$
30	29	unssbd	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to \{X\} \times f \subseteq t+ (R \cup (\{X\} \times f))$
31		imass1	$⊢ \{X\} \times f \subseteq t+ (R \cup (\{X\} \times f)) \to (\{X\} \times f) [\{X\}] \subseteq t+ (R \cup (\{X\} \times f)) [\{X\}]$
32	30 31	syl	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to (\{X\} \times f) [\{X\}] \subseteq t+ (R \cup (\{X\} \times f)) [\{X\}]$
33	28 32	eqsstrrd	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to f \subseteq t+ (R \cup (\{X\} \times f)) [\{X\}]$
34		imaundir	$⊢ (R \cup (\{X\} \times f)) [\{X\} \cup f] = R [\{X\} \cup f] \cup (\{X\} \times f) [\{X\} \cup f]$
35		simpr	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to R [\{X\} \cup f] \subseteq f$
36		imassrn	$⊢ (\{X\} \times f) [\{X\} \cup f] \subseteq ran (\{X\} \times f)$
37		rnxpss	$⊢ ran (\{X\} \times f) \subseteq f$
38	36 37	sstri	$⊢ (\{X\} \times f) [\{X\} \cup f] \subseteq f$
39	38	a1i	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to (\{X\} \times f) [\{X\} \cup f] \subseteq f$
40	35 39	unssd	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to R [\{X\} \cup f] \cup (\{X\} \times f) [\{X\} \cup f] \subseteq f$
41	34 40	eqsstrid	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to (R \cup (\{X\} \times f)) [\{X\} \cup f] \subseteq f$
42		trclimalb2	$⊢ (R \cup (\{X\} \times f) \in V \land (R \cup (\{X\} \times f)) [\{X\} \cup f] \subseteq f) \to t+ (R \cup (\{X\} \times f)) [\{X\}] \subseteq f$
43	16 41 42	syl2anc	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to t+ (R \cup (\{X\} \times f)) [\{X\}] \subseteq f$
44	33 43	eqssd	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to f = t+ (R \cup (\{X\} \times f)) [\{X\}]$
45		sbcan	$⊢ \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} ((R \subseteq r \land r \circ r \subseteq r) \land f = r [\{X\}]) \leftrightarrow (\underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} (R \subseteq r \land r \circ r \subseteq r) \land \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} f = r [\{X\}])$
46		sbcan	$⊢ \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} (R \subseteq r \land r \circ r \subseteq r) \leftrightarrow (\underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} R \subseteq r \land \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} r \circ r \subseteq r)$
47		fvex	$⊢ t+ (R \cup (\{X\} \times f)) \in V$
48		sbcssg	$⊢ t+ (R \cup (\{X\} \times f)) \in V \to (\underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} R \subseteq r \leftrightarrow ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ R \subseteq ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r)$
49	47 48	ax-mp	$⊢ \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} R \subseteq r \leftrightarrow ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ R \subseteq ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r$
50		csbconstg	$⊢ t+ (R \cup (\{X\} \times f)) \in V \to ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ R = R$
51	47 50	ax-mp	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ R = R$
52	47	csbvargi	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r = t+ (R \cup (\{X\} \times f))$
53	51 52	sseq12i	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ R \subseteq ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r \leftrightarrow R \subseteq t+ (R \cup (\{X\} \times f))$
54	49 53	bitri	$⊢ \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} R \subseteq r \leftrightarrow R \subseteq t+ (R \cup (\{X\} \times f))$
55		sbcssg	$⊢ t+ (R \cup (\{X\} \times f)) \in V \to (\underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} r \circ r \subseteq r \leftrightarrow ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ (r \circ r) \subseteq ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r)$
56	47 55	ax-mp	$⊢ \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} r \circ r \subseteq r \leftrightarrow ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ (r \circ r) \subseteq ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r$
57		csbcog	$⊢ t+ (R \cup (\{X\} \times f)) \in V \to ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ (r \circ r) = ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r \circ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r$
58	47 57	ax-mp	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ (r \circ r) = ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r \circ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r$
59	52 52	coeq12i	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r \circ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r = t+ (R \cup (\{X\} \times f)) \circ t+ (R \cup (\{X\} \times f))$
60	58 59	eqtri	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ (r \circ r) = t+ (R \cup (\{X\} \times f)) \circ t+ (R \cup (\{X\} \times f))$
61	60 52	sseq12i	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ (r \circ r) \subseteq ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r \leftrightarrow t+ (R \cup (\{X\} \times f)) \circ t+ (R \cup (\{X\} \times f)) \subseteq t+ (R \cup (\{X\} \times f))$
62	56 61	bitri	$⊢ \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} r \circ r \subseteq r \leftrightarrow t+ (R \cup (\{X\} \times f)) \circ t+ (R \cup (\{X\} \times f)) \subseteq t+ (R \cup (\{X\} \times f))$
63	54 62	anbi12i	$⊢ (\underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} R \subseteq r \land \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} r \circ r \subseteq r) \leftrightarrow (R \subseteq t+ (R \cup (\{X\} \times f)) \land t+ (R \cup (\{X\} \times f)) \circ t+ (R \cup (\{X\} \times f)) \subseteq t+ (R \cup (\{X\} \times f)))$
64	46 63	bitri	$⊢ \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} (R \subseteq r \land r \circ r \subseteq r) \leftrightarrow (R \subseteq t+ (R \cup (\{X\} \times f)) \land t+ (R \cup (\{X\} \times f)) \circ t+ (R \cup (\{X\} \times f)) \subseteq t+ (R \cup (\{X\} \times f)))$
65		sbceq2g	$⊢ t+ (R \cup (\{X\} \times f)) \in V \to (\underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} f = r [\{X\}] \leftrightarrow f = ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r [\{X\}])$
66	47 65	ax-mp	$⊢ \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} f = r [\{X\}] \leftrightarrow f = ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r [\{X\}]$
67		csbima12	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r [\{X\}] = ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r [⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ \{X\}]$
68	52	imaeq1i	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r [⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ \{X\}] = t+ (R \cup (\{X\} \times f)) [⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ \{X\}]$
69		csbconstg	$⊢ t+ (R \cup (\{X\} \times f)) \in V \to ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ \{X\} = \{X\}$
70	47 69	ax-mp	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ \{X\} = \{X\}$
71	70	imaeq2i	$⊢ t+ (R \cup (\{X\} \times f)) [⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ \{X\}] = t+ (R \cup (\{X\} \times f)) [\{X\}]$
72	67 68 71	3eqtri	$⊢ ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r [\{X\}] = t+ (R \cup (\{X\} \times f)) [\{X\}]$
73	72	eqeq2i	$⊢ f = ⦋ t+ (R \cup (\{X\} \times f)) / r ⦌ r [\{X\}] \leftrightarrow f = t+ (R \cup (\{X\} \times f)) [\{X\}]$
74	66 73	bitri	$⊢ \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} f = r [\{X\}] \leftrightarrow f = t+ (R \cup (\{X\} \times f)) [\{X\}]$
75	64 74	anbi12i	$⊢ (\underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} (R \subseteq r \land r \circ r \subseteq r) \land \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} f = r [\{X\}]) \leftrightarrow ((R \subseteq t+ (R \cup (\{X\} \times f)) \land t+ (R \cup (\{X\} \times f)) \circ t+ (R \cup (\{X\} \times f)) \subseteq t+ (R \cup (\{X\} \times f))) \land f = t+ (R \cup (\{X\} \times f)) [\{X\}])$
76	45 75	sylbbr	$⊢ ((R \subseteq t+ (R \cup (\{X\} \times f)) \land t+ (R \cup (\{X\} \times f)) \circ t+ (R \cup (\{X\} \times f)) \subseteq t+ (R \cup (\{X\} \times f))) \land f = t+ (R \cup (\{X\} \times f)) [\{X\}]) \to \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} ((R \subseteq r \land r \circ r \subseteq r) \land f = r [\{X\}])$
77	19 21 44 76	syl21anc	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to \underset{˙}{[} t+ (R \cup (\{X\} \times f)) / r \underset{˙}{]} ((R \subseteq r \land r \circ r \subseteq r) \land f = r [\{X\}])$
78	77	spesbcd	$⊢ ((X \in U \land Y \in V \land R \in W) \land R [\{X\} \cup f] \subseteq f) \to \exists r ((R \subseteq r \land r \circ r \subseteq r) \land f = r [\{X\}])$
79	78	ex	$⊢ (X \in U \land Y \in V \land R \in W) \to (R [\{X\} \cup f] \subseteq f \to \exists r ((R \subseteq r \land r \circ r \subseteq r) \land f = r [\{X\}]))$
80		eqeq1	$⊢ g = f \to (g = s [\{X\}] \leftrightarrow f = s [\{X\}])$
81	80	rexbidv	$⊢ g = f \to (\exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}] \leftrightarrow \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} f = s [\{X\}])$
82		imaeq1	$⊢ s = r \to s [\{X\}] = r [\{X\}]$
83	82	eqeq2d	$⊢ s = r \to (f = s [\{X\}] \leftrightarrow f = r [\{X\}])$
84	83	rexab2	$⊢ \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} f = s [\{X\}] \leftrightarrow \exists r ((R \subseteq r \land r \circ r \subseteq r) \land f = r [\{X\}])$
85	81 84	syl6bb	$⊢ g = f \to (\exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}] \leftrightarrow \exists r ((R \subseteq r \land r \circ r \subseteq r) \land f = r [\{X\}]))$
86	13 85	elab	$⊢ f \in \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\} \leftrightarrow \exists r ((R \subseteq r \land r \circ r \subseteq r) \land f = r [\{X\}])$
87	79 86	syl6ibr	$⊢ (X \in U \land Y \in V \land R \in W) \to (R [\{X\} \cup f] \subseteq f \to f \in \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\})$
88		intss1	$⊢ f \in \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\} \to ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\} \subseteq f$
89	87 88	syl6	$⊢ (X \in U \land Y \in V \land R \in W) \to (R [\{X\} \cup f] \subseteq f \to ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\} \subseteq f)$
90	89	alrimiv	$⊢ (X \in U \land Y \in V \land R \in W) \to \forall f (R [\{X\} \cup f] \subseteq f \to ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\} \subseteq f)$
91		ssintab	$⊢ ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\} \subseteq ⋂ \{f \| R [\{X\} \cup f] \subseteq f\} \leftrightarrow \forall f (R [\{X\} \cup f] \subseteq f \to ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\} \subseteq f)$
92	90 91	sylibr	$⊢ (X \in U \land Y \in V \land R \in W) \to ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\} \subseteq ⋂ \{f \| R [\{X\} \cup f] \subseteq f\}$
93		ssintab	$⊢ ⋂ \{f \| R [\{X\} \cup f] \subseteq f\} \subseteq ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\} \leftrightarrow \forall g (\exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}] \to ⋂ \{f \| R [\{X\} \cup f] \subseteq f\} \subseteq g)$
94	82	eqeq2d	$⊢ s = r \to (g = s [\{X\}] \leftrightarrow g = r [\{X\}])$
95	94	rexab2	$⊢ \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}] \leftrightarrow \exists r ((R \subseteq r \land r \circ r \subseteq r) \land g = r [\{X\}])$
96		simpr	$⊢ ((R \subseteq r \land r \circ r \subseteq r) \land g = r [\{X\}]) \to g = r [\{X\}]$
97		imass1	$⊢ R \subseteq r \to R [\{X\}] \subseteq r [\{X\}]$
98	97	adantr	$⊢ (R \subseteq r \land r \circ r \subseteq r) \to R [\{X\}] \subseteq r [\{X\}]$
99		imass1	$⊢ R \subseteq r \to R [r [\{X\}]] \subseteq r [r [\{X\}]]$
100		imaco	$⊢ (r \circ r) [\{X\}] = r [r [\{X\}]]$
101		imass1	$⊢ r \circ r \subseteq r \to (r \circ r) [\{X\}] \subseteq r [\{X\}]$
102	100 101	eqsstrrid	$⊢ r \circ r \subseteq r \to r [r [\{X\}]] \subseteq r [\{X\}]$
103	99 102	sylan9ss	$⊢ (R \subseteq r \land r \circ r \subseteq r) \to R [r [\{X\}]] \subseteq r [\{X\}]$
104	98 103	jca	$⊢ (R \subseteq r \land r \circ r \subseteq r) \to (R [\{X\}] \subseteq r [\{X\}] \land R [r [\{X\}]] \subseteq r [\{X\}])$
105	104	adantr	$⊢ ((R \subseteq r \land r \circ r \subseteq r) \land g = r [\{X\}]) \to (R [\{X\}] \subseteq r [\{X\}] \land R [r [\{X\}]] \subseteq r [\{X\}])$
106		vex	$⊢ r \in V$
107	106	imaex	$⊢ r [\{X\}] \in V$
108		imaundi	$⊢ R [\{X\} \cup f] = R [\{X\}] \cup R [f]$
109	108	sseq1i	$⊢ R [\{X\} \cup f] \subseteq f \leftrightarrow R [\{X\}] \cup R [f] \subseteq f$
110		unss	$⊢ (R [\{X\}] \subseteq f \land R [f] \subseteq f) \leftrightarrow R [\{X\}] \cup R [f] \subseteq f$
111	109 110	bitr4i	$⊢ R [\{X\} \cup f] \subseteq f \leftrightarrow (R [\{X\}] \subseteq f \land R [f] \subseteq f)$
112		imaeq2	$⊢ f = r [\{X\}] \to R [f] = R [r [\{X\}]]$
113		id	$⊢ f = r [\{X\}] \to f = r [\{X\}]$
114	112 113	sseq12d	$⊢ f = r [\{X\}] \to (R [f] \subseteq f \leftrightarrow R [r [\{X\}]] \subseteq r [\{X\}])$
115	114	cleq2lem	$⊢ f = r [\{X\}] \to ((R [\{X\}] \subseteq f \land R [f] \subseteq f) \leftrightarrow (R [\{X\}] \subseteq r [\{X\}] \land R [r [\{X\}]] \subseteq r [\{X\}]))$
116	111 115	syl5bb	$⊢ f = r [\{X\}] \to (R [\{X\} \cup f] \subseteq f \leftrightarrow (R [\{X\}] \subseteq r [\{X\}] \land R [r [\{X\}]] \subseteq r [\{X\}]))$
117	107 116	elab	$⊢ r [\{X\}] \in \{f \| R [\{X\} \cup f] \subseteq f\} \leftrightarrow (R [\{X\}] \subseteq r [\{X\}] \land R [r [\{X\}]] \subseteq r [\{X\}])$
118	105 117	sylibr	$⊢ ((R \subseteq r \land r \circ r \subseteq r) \land g = r [\{X\}]) \to r [\{X\}] \in \{f \| R [\{X\} \cup f] \subseteq f\}$
119	96 118	eqeltrd	$⊢ ((R \subseteq r \land r \circ r \subseteq r) \land g = r [\{X\}]) \to g \in \{f \| R [\{X\} \cup f] \subseteq f\}$
120	119	exlimiv	$⊢ \exists r ((R \subseteq r \land r \circ r \subseteq r) \land g = r [\{X\}]) \to g \in \{f \| R [\{X\} \cup f] \subseteq f\}$
121	95 120	sylbi	$⊢ \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}] \to g \in \{f \| R [\{X\} \cup f] \subseteq f\}$
122		intss1	$⊢ g \in \{f \| R [\{X\} \cup f] \subseteq f\} \to ⋂ \{f \| R [\{X\} \cup f] \subseteq f\} \subseteq g$
123	121 122	syl	$⊢ \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}] \to ⋂ \{f \| R [\{X\} \cup f] \subseteq f\} \subseteq g$
124	93 123	mpgbir	$⊢ ⋂ \{f \| R [\{X\} \cup f] \subseteq f\} \subseteq ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\}$
125	124	a1i	$⊢ (X \in U \land Y \in V \land R \in W) \to ⋂ \{f \| R [\{X\} \cup f] \subseteq f\} \subseteq ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\}$
126	92 125	eqssd	$⊢ (X \in U \land Y \in V \land R \in W) \to ⋂ \{g \| \exists s \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} g = s [\{X\}]\} = ⋂ \{f \| R [\{X\} \cup f] \subseteq f\}$
127	10 126	eqtrd	$⊢ (X \in U \land Y \in V \land R \in W) \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} [\{X\}] = ⋂ \{f \| R [\{X\} \cup f] \subseteq f\}$
128	127	eleq2d	$⊢ (X \in U \land Y \in V \land R \in W) \to (Y \in ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} [\{X\}] \leftrightarrow Y \in ⋂ \{f \| R [\{X\} \cup f] \subseteq f\})$
129	8 128	bitrd	$⊢ (X \in U \land Y \in V \land R \in W) \to (X t+ (R) Y \leftrightarrow Y \in ⋂ \{f \| R [\{X\} \cup f] \subseteq f\})$

Metamath Proof Explorer

Theorem brtrclfv2

Proof