dftrcl3

Description: Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020)

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

Proof

Step	Hyp	Ref	Expression
1		df-trcl	$⊢ t+ = (r \in V ⟼ ⋂ \{z \| (r \subseteq z \land z \circ z \subseteq z)\})$
2		relexp1g	$⊢ r \in V \to r ↑_{r} 1 = r$
3		nnex	$⊢ ℕ \in V$
4		1nn	$⊢ 1 \in ℕ$
5		oveq1	$⊢ a = t \to a ↑_{r} n = t ↑_{r} n$
6	5	iuneq2d	$⊢ a = t \to ⋃_{n \in ℕ} (a ↑_{r} n) = ⋃_{n \in ℕ} (t ↑_{r} n)$
7		oveq2	$⊢ n = k \to t ↑_{r} n = t ↑_{r} k$
8	7	cbviunv	$⊢ ⋃_{n \in ℕ} (t ↑_{r} n) = ⋃_{k \in ℕ} (t ↑_{r} k)$
9	6 8	syl6eq	$⊢ a = t \to ⋃_{n \in ℕ} (a ↑_{r} n) = ⋃_{k \in ℕ} (t ↑_{r} k)$
10	9	cbvmptv	$⊢ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) = (t \in V ⟼ ⋃_{k \in ℕ} (t ↑_{r} k))$
11	10	ov2ssiunov2	$⊢ (r \in V \land ℕ \in V \land 1 \in ℕ) \to r ↑_{r} 1 \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)$
12	3 4 11	mp3an23	$⊢ r \in V \to r ↑_{r} 1 \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)$
13	2 12	eqsstrrd	$⊢ r \in V \to r \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)$
14		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
15		1nn0	$⊢ 1 \in ℕ_{0}$
16	10	iunrelexpuztr	$⊢ (r \in V \land ℕ = ℤ_{\geq 1} \land 1 \in ℕ_{0}) \to (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)$
17	14 15 16	mp3an23	$⊢ r \in V \to (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)$
18		fvex	$⊢ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \in V$
19		trcleq2lem	$⊢ z = (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \to ((r \subseteq z \land z \circ z \subseteq z) \leftrightarrow (r \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)))$
20	19	a1i	$⊢ r \in V \to (z = (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \to ((r \subseteq z \land z \circ z \subseteq z) \leftrightarrow (r \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r))))$
21	20	alrimiv	$⊢ r \in V \to \forall z (z = (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \to ((r \subseteq z \land z \circ z \subseteq z) \leftrightarrow (r \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r))))$
22		elabgt	$⊢ ((a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \in V \land \forall z (z = (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \to ((r \subseteq z \land z \circ z \subseteq z) \leftrightarrow (r \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r))))) \to ((a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \in \{z \| (r \subseteq z \land z \circ z \subseteq z)\} \leftrightarrow (r \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)))$
23	18 21 22	sylancr	$⊢ r \in V \to ((a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \in \{z \| (r \subseteq z \land z \circ z \subseteq z)\} \leftrightarrow (r \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \land (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \circ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)))$
24	13 17 23	mpbir2and	$⊢ r \in V \to (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \in \{z \| (r \subseteq z \land z \circ z \subseteq z)\}$
25		intss1	$⊢ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \in \{z \| (r \subseteq z \land z \circ z \subseteq z)\} \to ⋂ \{z \| (r \subseteq z \land z \circ z \subseteq z)\} \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)$
26	24 25	syl	$⊢ r \in V \to ⋂ \{z \| (r \subseteq z \land z \circ z \subseteq z)\} \subseteq (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)$
27		vex	$⊢ s \in V$
28		trcleq2lem	$⊢ z = s \to ((r \subseteq z \land z \circ z \subseteq z) \leftrightarrow (r \subseteq s \land s \circ s \subseteq s))$
29	27 28	elab	$⊢ s \in \{z \| (r \subseteq z \land z \circ z \subseteq z)\} \leftrightarrow (r \subseteq s \land s \circ s \subseteq s)$
30		eqid	$⊢ ℕ = ℕ$
31	10	iunrelexpmin1	$⊢ (r \in V \land ℕ = ℕ) \to \forall s ((r \subseteq s \land s \circ s \subseteq s) \to (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq s)$
32	30 31	mpan2	$⊢ r \in V \to \forall s ((r \subseteq s \land s \circ s \subseteq s) \to (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq s)$
33	32	19.21bi	$⊢ r \in V \to ((r \subseteq s \land s \circ s \subseteq s) \to (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq s)$
34	29 33	syl5bi	$⊢ r \in V \to (s \in \{z \| (r \subseteq z \land z \circ z \subseteq z)\} \to (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq s)$
35	34	ralrimiv	$⊢ r \in V \to \forall s \in \{z \| (r \subseteq z \land z \circ z \subseteq z)\} (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq s$
36		ssint	$⊢ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq ⋂ \{z \| (r \subseteq z \land z \circ z \subseteq z)\} \leftrightarrow \forall s \in \{z \| (r \subseteq z \land z \circ z \subseteq z)\} (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq s$
37	35 36	sylibr	$⊢ r \in V \to (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) \subseteq ⋂ \{z \| (r \subseteq z \land z \circ z \subseteq z)\}$
38	26 37	eqssd	$⊢ r \in V \to ⋂ \{z \| (r \subseteq z \land z \circ z \subseteq z)\} = (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r)$
39		oveq1	$⊢ a = r \to a ↑_{r} n = r ↑_{r} n$
40	39	iuneq2d	$⊢ a = r \to ⋃_{n \in ℕ} (a ↑_{r} n) = ⋃_{n \in ℕ} (r ↑_{r} n)$
41		eqid	$⊢ (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) = (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n))$
42		ovex	$⊢ r ↑_{r} n \in V$
43	3 42	iunex	$⊢ ⋃_{n \in ℕ} (r ↑_{r} n) \in V$
44	40 41 43	fvmpt	$⊢ r \in V \to (a \in V ⟼ ⋃_{n \in ℕ} (a ↑_{r} n)) (r) = ⋃_{n \in ℕ} (r ↑_{r} n)$
45	38 44	eqtrd	$⊢ r \in V \to ⋂ \{z \| (r \subseteq z \land z \circ z \subseteq z)\} = ⋃_{n \in ℕ} (r ↑_{r} n)$
46	45	mpteq2ia	$⊢ (r \in V ⟼ ⋂ \{z \| (r \subseteq z \land z \circ z \subseteq z)\}) = (r \in V ⟼ ⋃_{n \in ℕ} (r ↑_{r} n))$
47	1 46	eqtri	$⊢ t+ = (r \in V ⟼ ⋃_{n \in ℕ} (r ↑_{r} n))$

Metamath Proof Explorer

Theorem dftrcl3

Proof