dfrtrcl2

Description: The two definitions t* and t*rec of the reflexive, transitive closure coincide if R is indeed a relation. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 13-Jul-2024)

		Ref	Expression
	Hypothesis	dfrtrcl2.1	$⊢ φ \to Rel R$
	Assertion	dfrtrcl2	$⊢ φ \to t* (R) = t*rec (R)$

Proof

Step	Hyp	Ref	Expression
1		dfrtrcl2.1	$⊢ φ \to Rel R$
2		eqidd	$⊢ (φ \land R \in V) \to (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}) = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\})$
3		dmeq	$⊢ x = R \to dom x = dom R$
4		rneq	$⊢ x = R \to ran x = ran R$
5	3 4	uneq12d	$⊢ x = R \to dom x \cup ran x = dom R \cup ran R$
6	5	reseq2d	$⊢ x = R \to {I ↾}_{(dom x \cup ran x)} = {I ↾}_{(dom R \cup ran R)}$
7	6	sseq1d	$⊢ x = R \to ({I ↾}_{(dom x \cup ran x)} \subseteq z \leftrightarrow {I ↾}_{(dom R \cup ran R)} \subseteq z)$
8		id	$⊢ x = R \to x = R$
9	8	sseq1d	$⊢ x = R \to (x \subseteq z \leftrightarrow R \subseteq z)$
10	7 9	3anbi12d	$⊢ x = R \to (({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z) \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z))$
11	10	abbidv	$⊢ x = R \to \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\} = \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\}$
12	11	inteqd	$⊢ x = R \to ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\} = ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\}$
13	12	adantl	$⊢ ((φ \land R \in V) \land x = R) \to ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\} = ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\}$
14		simpr	$⊢ (φ \land R \in V) \to R \in V$
15		relfld	$⊢ Rel R \to ⋃ ⋃ R = dom R \cup ran R$
16	1 15	syl	$⊢ φ \to ⋃ ⋃ R = dom R \cup ran R$
17	16	eqcomd	$⊢ φ \to dom R \cup ran R = ⋃ ⋃ R$
18	17	adantr	$⊢ (φ \land R \in V) \to dom R \cup ran R = ⋃ ⋃ R$
19	1	adantr	$⊢ (φ \land R \in V) \to Rel R$
20	19 14	rtrclreclem2	$⊢ (φ \land R \in V) \to {I ↾}_{⋃ ⋃ R} \subseteq t*rec (R)$
21		id	$⊢ dom R \cup ran R = ⋃ ⋃ R \to dom R \cup ran R = ⋃ ⋃ R$
22	21	reseq2d	$⊢ dom R \cup ran R = ⋃ ⋃ R \to {I ↾}_{(dom R \cup ran R)} = {I ↾}_{⋃ ⋃ R}$
23	22	sseq1d	$⊢ dom R \cup ran R = ⋃ ⋃ R \to ({I ↾}_{(dom R \cup ran R)} \subseteq trec (R) \leftrightarrow {I ↾}_{⋃ ⋃ R} \subseteq trec (R))$
24	20 23	imbitrrid	$⊢ dom R \cup ran R = ⋃ ⋃ R \to ((φ \land R \in V) \to {I ↾}_{(dom R \cup ran R)} \subseteq t*rec (R))$
25	18 24	mpcom	$⊢ (φ \land R \in V) \to {I ↾}_{(dom R \cup ran R)} \subseteq t*rec (R)$
26	14	rtrclreclem1	$⊢ (φ \land R \in V) \to R \subseteq t*rec (R)$
27	1	rtrclreclem3	$⊢ φ \to trec (R) \circ trec (R) \subseteq t*rec (R)$
28	27	adantr	$⊢ (φ \land R \in V) \to trec (R) \circ trec (R) \subseteq t*rec (R)$
29		fvex	$⊢ t*rec (R) \in V$
30		sseq2	$⊢ z = trec (R) \to ({I ↾}_{(dom R \cup ran R)} \subseteq z \leftrightarrow {I ↾}_{(dom R \cup ran R)} \subseteq trec (R))$
31		sseq2	$⊢ z = trec (R) \to (R \subseteq z \leftrightarrow R \subseteq trec (R))$
32		id	$⊢ z = trec (R) \to z = trec (R)$
33	32 32	coeq12d	$⊢ z = trec (R) \to z \circ z = trec (R) \circ t*rec (R)$
34	33 32	sseq12d	$⊢ z = trec (R) \to (z \circ z \subseteq z \leftrightarrow trec (R) \circ trec (R) \subseteq trec (R))$
35	30 31 34	3anbi123d	$⊢ z = trec (R) \to (({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z) \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq trec (R) \land R \subseteq trec (R) \land trec (R) \circ trec (R) \subseteq trec (R)))$
36	35	a1i	$⊢ φ \to (z = trec (R) \to (({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z) \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq trec (R) \land R \subseteq trec (R) \land trec (R) \circ trec (R) \subseteq trec (R))))$
37	36	alrimiv	$⊢ φ \to \forall z (z = trec (R) \to (({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z) \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq trec (R) \land R \subseteq trec (R) \land trec (R) \circ trec (R) \subseteq trec (R))))$
38		elabgt	$⊢ (trec (R) \in V \land \forall z (z = trec (R) \to (({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z) \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq trec (R) \land R \subseteq trec (R) \land trec (R) \circ trec (R) \subseteq trec (R))))) \to (trec (R) \in \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq trec (R) \land R \subseteq trec (R) \land trec (R) \circ trec (R) \subseteq t*rec (R)))$
39	29 37 38	sylancr	$⊢ φ \to (trec (R) \in \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq trec (R) \land R \subseteq trec (R) \land trec (R) \circ trec (R) \subseteq trec (R)))$
40	39	adantr	$⊢ (φ \land R \in V) \to (trec (R) \in \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq trec (R) \land R \subseteq trec (R) \land trec (R) \circ trec (R) \subseteq trec (R)))$
41	25 26 28 40	mpbir3and	$⊢ (φ \land R \in V) \to t*rec (R) \in \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\}$
42	41	ne0d	$⊢ (φ \land R \in V) \to \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \neq \emptyset$
43		intex	$⊢ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \neq \emptyset \leftrightarrow ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \in V$
44	42 43	sylib	$⊢ (φ \land R \in V) \to ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \in V$
45	2 13 14 44	fvmptd	$⊢ (φ \land R \in V) \to (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}) (R) = ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\}$
46		intss1	$⊢ trec (R) \in \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \to ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \subseteq trec (R)$
47	41 46	syl	$⊢ (φ \land R \in V) \to ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \subseteq t*rec (R)$
48		vex	$⊢ s \in V$
49		sseq2	$⊢ z = s \to ({I ↾}_{(dom R \cup ran R)} \subseteq z \leftrightarrow {I ↾}_{(dom R \cup ran R)} \subseteq s)$
50		sseq2	$⊢ z = s \to (R \subseteq z \leftrightarrow R \subseteq s)$
51		id	$⊢ z = s \to z = s$
52	51 51	coeq12d	$⊢ z = s \to z \circ z = s \circ s$
53	52 51	sseq12d	$⊢ z = s \to (z \circ z \subseteq z \leftrightarrow s \circ s \subseteq s)$
54	49 50 53	3anbi123d	$⊢ z = s \to (({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z) \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s))$
55	48 54	elab	$⊢ s \in \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s)$
56	1	rtrclreclem4	$⊢ φ \to \forall s (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to t*rec (R) \subseteq s)$
57	56	19.21bi	$⊢ φ \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to t*rec (R) \subseteq s)$
58	55 57	biimtrid	$⊢ φ \to (s \in \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \to t*rec (R) \subseteq s)$
59	58	ralrimiv	$⊢ φ \to \forall s \in \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} t*rec (R) \subseteq s$
60		ssint	$⊢ trec (R) \subseteq ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} \leftrightarrow \forall s \in \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} trec (R) \subseteq s$
61	59 60	sylibr	$⊢ φ \to t*rec (R) \subseteq ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\}$
62	61	adantr	$⊢ (φ \land R \in V) \to t*rec (R) \subseteq ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\}$
63	47 62	eqssd	$⊢ (φ \land R \in V) \to ⋂ \{z \| ({I ↾}_{(dom R \cup ran R)} \subseteq z \land R \subseteq z \land z \circ z \subseteq z)\} = t*rec (R)$
64	45 63	eqtrd	$⊢ (φ \land R \in V) \to (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}) (R) = t*rec (R)$
65		df-rtrcl	$⊢ t* = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\})$
66		fveq1	$⊢ t* = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}) \to t* (R) = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}) (R)$
67	66	eqeq1d	$⊢ t* = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}) \to (t* (R) = trec (R) \leftrightarrow (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}) (R) = trec (R))$
68	67	imbi2d	$⊢ t* = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}) \to (((φ \land R \in V) \to t* (R) = trec (R)) \leftrightarrow ((φ \land R \in V) \to (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}) (R) = trec (R)))$
69	65 68	ax-mp	$⊢ ((φ \land R \in V) \to t* (R) = trec (R)) \leftrightarrow ((φ \land R \in V) \to (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}) (R) = trec (R))$
70	64 69	mpbir	$⊢ (φ \land R \in V) \to t* (R) = t*rec (R)$
71	70	ex	$⊢ φ \to (R \in V \to t* (R) = t*rec (R))$
72		fvprc	$⊢ \neg R \in V \to t* (R) = \emptyset$
73		fvprc	$⊢ \neg R \in V \to t*rec (R) = \emptyset$
74	73	eqcomd	$⊢ \neg R \in V \to \emptyset = t*rec (R)$
75	72 74	eqtrd	$⊢ \neg R \in V \to t* (R) = t*rec (R)$
76	71 75	pm2.61d1	$⊢ φ \to t* (R) = t*rec (R)$

Metamath Proof Explorer

Theorem dfrtrcl2

Proof