cotrcltrcl

Description: The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020)

		Ref	Expression
	Assertion	cotrcltrcl	$⊢ t+ \circ t+ = t+$

Proof

Step	Hyp	Ref	Expression
1		dftrcl3	$⊢ t+ = (a \in V ⟼ ⋃_{i \in ℕ} (a ↑_{r} i))$
2		dftrcl3	$⊢ t+ = (b \in V ⟼ ⋃_{j \in ℕ} (b ↑_{r} j))$
3		dftrcl3	$⊢ t+ = (c \in V ⟼ ⋃_{k \in ℕ} (c ↑_{r} k))$
4		nnex	$⊢ ℕ \in V$
5		unidm	$⊢ ℕ \cup ℕ = ℕ$
6	5	eqcomi	$⊢ ℕ = ℕ \cup ℕ$
7		1ex	$⊢ 1 \in V$
8		oveq2	$⊢ i = 1 \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1$
9	7 8	iunxsn	$⊢ ⋃_{i \in \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1$
10		ovex	$⊢ d ↑_{r} j \in V$
11	4 10	iunex	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) \in V$
12		relexp1g	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) \in V \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1 = ⋃_{j \in ℕ} (d ↑_{r} j)$
13	11 12	ax-mp	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1 = ⋃_{j \in ℕ} (d ↑_{r} j)$
14		oveq2	$⊢ j = k \to d ↑_{r} j = d ↑_{r} k$
15	14	cbviunv	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) = ⋃_{k \in ℕ} (d ↑_{r} k)$
16	13 15	eqtri	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1 = ⋃_{k \in ℕ} (d ↑_{r} k)$
17	9 16	eqtri	$⊢ ⋃_{i \in \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = ⋃_{k \in ℕ} (d ↑_{r} k)$
18	17	eqcomi	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) = ⋃_{i \in \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
19		1nn	$⊢ 1 \in ℕ$
20		snssi	$⊢ 1 \in ℕ \to \{1\} \subseteq ℕ$
21		iunss1	$⊢ \{1\} \subseteq ℕ \to ⋃_{i \in \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) \subseteq ⋃_{i \in ℕ} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
22	19 20 21	mp2b	$⊢ ⋃_{i \in \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) \subseteq ⋃_{i \in ℕ} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
23	18 22	eqsstri	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) \subseteq ⋃_{i \in ℕ} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
24		iunss	$⊢ ⋃_{i \in ℕ} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k) \leftrightarrow \forall i \in ℕ ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)$
25		oveq2	$⊢ x = 1 \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} x = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1$
26	25	sseq1d	$⊢ x = 1 \to (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} x \subseteq ⋃_{k \in ℕ} (d ↑_{r} k) \leftrightarrow ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1 \subseteq ⋃_{k \in ℕ} (d ↑_{r} k))$
27		oveq2	$⊢ x = y \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} x = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y$
28	27	sseq1d	$⊢ x = y \to (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} x \subseteq ⋃_{k \in ℕ} (d ↑_{r} k) \leftrightarrow ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y \subseteq ⋃_{k \in ℕ} (d ↑_{r} k))$
29		oveq2	$⊢ x = y + 1 \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} x = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} (y + 1)$
30	29	sseq1d	$⊢ x = y + 1 \to (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} x \subseteq ⋃_{k \in ℕ} (d ↑_{r} k) \leftrightarrow ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} (y + 1) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k))$
31		oveq2	$⊢ x = i \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} x = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i$
32	31	sseq1d	$⊢ x = i \to (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} x \subseteq ⋃_{k \in ℕ} (d ↑_{r} k) \leftrightarrow ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i \subseteq ⋃_{k \in ℕ} (d ↑_{r} k))$
33	16	eqimssi	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1 \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)$
34		simpl	$⊢ (y \in ℕ \land ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)) \to y \in ℕ$
35		relexpsucnnr	$⊢ (⋃_{j \in ℕ} (d ↑_{r} j) \in V \land y \in ℕ) \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} (y + 1) = (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y) \circ ⋃_{j \in ℕ} (d ↑_{r} j)$
36	11 34 35	sylancr	$⊢ (y \in ℕ \land ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)) \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} (y + 1) = (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y) \circ ⋃_{j \in ℕ} (d ↑_{r} j)$
37		coss1	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y \subseteq ⋃_{k \in ℕ} (d ↑_{r} k) \to (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y) \circ ⋃_{j \in ℕ} (d ↑_{r} j) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k) \circ ⋃_{j \in ℕ} (d ↑_{r} j)$
38	37	adantl	$⊢ (y \in ℕ \land ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)) \to (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y) \circ ⋃_{j \in ℕ} (d ↑_{r} j) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k) \circ ⋃_{j \in ℕ} (d ↑_{r} j)$
39	15	coeq2i	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) \circ ⋃_{j \in ℕ} (d ↑_{r} j) = ⋃_{k \in ℕ} (d ↑_{r} k) \circ ⋃_{k \in ℕ} (d ↑_{r} k)$
40		trclfvcotrg	$⊢ t+ (d) \circ t+ (d) \subseteq t+ (d)$
41		oveq1	$⊢ c = d \to c ↑_{r} k = d ↑_{r} k$
42	41	iuneq2d	$⊢ c = d \to ⋃_{k \in ℕ} (c ↑_{r} k) = ⋃_{k \in ℕ} (d ↑_{r} k)$
43		ovex	$⊢ d ↑_{r} k \in V$
44	4 43	iunex	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) \in V$
45	42 3 44	fvmpt	$⊢ d \in V \to t+ (d) = ⋃_{k \in ℕ} (d ↑_{r} k)$
46	45	elv	$⊢ t+ (d) = ⋃_{k \in ℕ} (d ↑_{r} k)$
47	46 46	coeq12i	$⊢ t+ (d) \circ t+ (d) = ⋃_{k \in ℕ} (d ↑_{r} k) \circ ⋃_{k \in ℕ} (d ↑_{r} k)$
48	40 47 46	3sstr3i	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) \circ ⋃_{k \in ℕ} (d ↑_{r} k) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)$
49	39 48	eqsstri	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) \circ ⋃_{j \in ℕ} (d ↑_{r} j) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)$
50	38 49	sstrdi	$⊢ (y \in ℕ \land ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)) \to (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y) \circ ⋃_{j \in ℕ} (d ↑_{r} j) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)$
51	36 50	eqsstrd	$⊢ (y \in ℕ \land ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)) \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} (y + 1) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)$
52	51	ex	$⊢ y \in ℕ \to (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} y \subseteq ⋃_{k \in ℕ} (d ↑_{r} k) \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} (y + 1) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k))$
53	26 28 30 32 33 52	nnind	$⊢ i \in ℕ \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)$
54	24 53	mprgbir	$⊢ ⋃_{i \in ℕ} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)$
55		iuneq1	$⊢ ℕ = ℕ \cup ℕ \to ⋃_{k \in ℕ} (d ↑_{r} k) = ⋃_{k \in ℕ \cup ℕ} (d ↑_{r} k)$
56	6 55	ax-mp	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) = ⋃_{k \in ℕ \cup ℕ} (d ↑_{r} k)$
57	54 56	sseqtri	$⊢ ⋃_{i \in ℕ} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) \subseteq ⋃_{k \in ℕ \cup ℕ} (d ↑_{r} k)$
58	1 2 3 4 4 6 23 23 57	comptiunov2i	$⊢ t+ \circ t+ = t+$

Metamath Proof Explorer

Theorem cotrcltrcl

Proof