dfrtrcl3

Description: Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 . (Contributed by RP, 5-Jun-2020)

		Ref	Expression
	Assertion	dfrtrcl3	$⊢ t* = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n))$

Proof

Step	Hyp	Ref	Expression
1		df-rtrcl	$⊢ t* = (r \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom r \cup ran r)} \subseteq z \land r \subseteq z \land z \circ z \subseteq z)\})$
2		relexp0g	$⊢ r \in V \to r ↑_{r} 0 = {I ↾}_{(dom r \cup ran r)}$
3		nn0ex	$⊢ ℕ_{0} \in V$
4		0nn0	$⊢ 0 \in ℕ_{0}$
5		oveq1	$⊢ a = t \to a ↑_{r} n = t ↑_{r} n$
6	5	iuneq2d	$⊢ a = t \to ⋃_{n \in ℕ_{0}} (a ↑_{r} n) = ⋃_{n \in ℕ_{0}} (t ↑_{r} n)$
7		oveq2	$⊢ n = k \to t ↑_{r} n = t ↑_{r} k$
8	7	cbviunv	$⊢ ⋃_{n \in ℕ_{0}} (t ↑_{r} n) = ⋃_{k \in ℕ_{0}} (t ↑_{r} k)$
9	6 8	eqtrdi	$⊢ a = t \to ⋃_{n \in ℕ_{0}} (a ↑_{r} n) = ⋃_{k \in ℕ_{0}} (t ↑_{r} k)$
10	9	cbvmptv	$⊢ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) = (t \in V ⟼ ⋃_{k \in ℕ_{0}} (t ↑_{r} k))$
11	10	ov2ssiunov2	$⊢ (r \in V \land ℕ_{0} \in V \land 0 \in ℕ_{0}) \to r ↑_{r} 0 \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
12	3 4 11	mp3an23	$⊢ r \in V \to r ↑_{r} 0 \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
13	2 12	eqsstrrd	$⊢ r \in V \to {I ↾}_{(dom r \cup ran r)} \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
14		relexp1g	$⊢ r \in V \to r ↑_{r} 1 = r$
15		1nn0	$⊢ 1 \in ℕ_{0}$
16	10	ov2ssiunov2	$⊢ (r \in V \land ℕ_{0} \in V \land 1 \in ℕ_{0}) \to r ↑_{r} 1 \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
17	3 15 16	mp3an23	$⊢ r \in V \to r ↑_{r} 1 \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
18	14 17	eqsstrrd	$⊢ r \in V \to r \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
19		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
20	10	iunrelexpuztr	$⊢ (r \in V \land ℕ_{0} = ℤ_{\geq 0} \land 0 \in ℕ_{0}) \to (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
21	19 4 20	mp3an23	$⊢ r \in V \to (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
22		fvex	$⊢ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \in V$
23		sseq2	$⊢ z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \to ({I ↾}_{(dom r \cup ran r)} \subseteq z \leftrightarrow {I ↾}_{(dom r \cup ran r)} \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r))$
24		sseq2	$⊢ z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \to (r \subseteq z \leftrightarrow r \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r))$
25		id	$⊢ z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \to z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
26	25 25	coeq12d	$⊢ z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \to z \circ z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
27	26 25	sseq12d	$⊢ z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \to (z \circ z \subseteq z \leftrightarrow (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r))$
28	23 24 27	3anbi123d	$⊢ z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (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 (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land r \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)))$
29	28	a1i	$⊢ r \in V \to (z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (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 (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land r \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r))))$
30	29	alrimiv	$⊢ r \in V \to \forall z (z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (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 (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land r \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r))))$
31		elabgt	$⊢ ((a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \in V \land \forall z (z = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (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 (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land r \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r))))) \to ((a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (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 (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land r \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)))$
32	22 30 31	sylancr	$⊢ r \in V \to ((a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (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 (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land r \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)))$
33	13 18 21 32	mpbir3and	$⊢ r \in V \to (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \in \{z \| ({I ↾}_{(dom r \cup ran r)} \subseteq z \land r \subseteq z \land z \circ z \subseteq z)\}$
34		intss1	$⊢ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (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 (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
35	33 34	syl	$⊢ r \in V \to ⋂ \{z \| ({I ↾}_{(dom r \cup ran r)} \subseteq z \land r \subseteq z \land z \circ z \subseteq z)\} \subseteq (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
36		vex	$⊢ s \in V$
37		sseq2	$⊢ z = s \to ({I ↾}_{(dom r \cup ran r)} \subseteq z \leftrightarrow {I ↾}_{(dom r \cup ran r)} \subseteq s)$
38		sseq2	$⊢ z = s \to (r \subseteq z \leftrightarrow r \subseteq s)$
39		id	$⊢ z = s \to z = s$
40	39 39	coeq12d	$⊢ z = s \to z \circ z = s \circ s$
41	40 39	sseq12d	$⊢ z = s \to (z \circ z \subseteq z \leftrightarrow s \circ s \subseteq s)$
42	37 38 41	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))$
43	36 42	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)$
44		eqid	$⊢ ℕ_{0} = ℕ_{0}$
45	10	iunrelexpmin2	$⊢ (r \in V \land ℕ_{0} = ℕ_{0}) \to \forall s (({I ↾}_{(dom r \cup ran r)} \subseteq s \land r \subseteq s \land s \circ s \subseteq s) \to (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq s)$
46	44 45	mpan2	$⊢ r \in V \to \forall s (({I ↾}_{(dom r \cup ran r)} \subseteq s \land r \subseteq s \land s \circ s \subseteq s) \to (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq s)$
47	46	19.21bi	$⊢ r \in V \to (({I ↾}_{(dom r \cup ran r)} \subseteq s \land r \subseteq s \land s \circ s \subseteq s) \to (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq s)$
48	43 47	syl5bi	$⊢ r \in V \to (s \in \{z \| ({I ↾}_{(dom r \cup ran r)} \subseteq z \land r \subseteq z \land z \circ z \subseteq z)\} \to (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq s)$
49	48	ralrimiv	$⊢ r \in V \to \forall s \in \{z \| ({I ↾}_{(dom r \cup ran r)} \subseteq z \land r \subseteq z \land z \circ z \subseteq z)\} (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq s$
50		ssint	$⊢ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (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)\} (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq s$
51	49 50	sylibr	$⊢ r \in V \to (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) \subseteq ⋂ \{z \| ({I ↾}_{(dom r \cup ran r)} \subseteq z \land r \subseteq z \land z \circ z \subseteq z)\}$
52	35 51	eqssd	$⊢ r \in V \to ⋂ \{z \| ({I ↾}_{(dom r \cup ran r)} \subseteq z \land r \subseteq z \land z \circ z \subseteq z)\} = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r)$
53		oveq1	$⊢ a = r \to a ↑_{r} n = r ↑_{r} n$
54	53	iuneq2d	$⊢ a = r \to ⋃_{n \in ℕ_{0}} (a ↑_{r} n) = ⋃_{n \in ℕ_{0}} (r ↑_{r} n)$
55		eqid	$⊢ (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) = (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n))$
56		ovex	$⊢ r ↑_{r} n \in V$
57	3 56	iunex	$⊢ ⋃_{n \in ℕ_{0}} (r ↑_{r} n) \in V$
58	54 55 57	fvmpt	$⊢ r \in V \to (a \in V ⟼ ⋃_{n \in ℕ_{0}} (a ↑_{r} n)) (r) = ⋃_{n \in ℕ_{0}} (r ↑_{r} n)$
59	52 58	eqtrd	$⊢ r \in V \to ⋂ \{z \| ({I ↾}_{(dom r \cup ran r)} \subseteq z \land r \subseteq z \land z \circ z \subseteq z)\} = ⋃_{n \in ℕ_{0}} (r ↑_{r} n)$
60	59	mpteq2ia	$⊢ (r \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom r \cup ran r)} \subseteq z \land r \subseteq z \land z \circ z \subseteq z)\}) = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n))$
61	1 60	eqtri	$⊢ t* = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n))$

Metamath Proof Explorer

Theorem dfrtrcl3

Proof