corcltrcl

Description: The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 17-Jun-2020)

		Ref	Expression
	Assertion	corcltrcl	$⊢ r* \circ t+ = t*$

Proof

Step	Hyp	Ref	Expression
1		dfrcl4	$⊢ r* = (a \in V ⟼ ⋃_{i \in \{0, 1\}} (a ↑_{r} i))$
2		dftrcl3	$⊢ t+ = (b \in V ⟼ ⋃_{j \in ℕ} (b ↑_{r} j))$
3		dfrtrcl3	$⊢ t* = (c \in V ⟼ ⋃_{k \in ℕ_{0}} (c ↑_{r} k))$
4		prex	$⊢ \{0, 1\} \in V$
5		nnex	$⊢ ℕ \in V$
6		df-n0	$⊢ ℕ_{0} = ℕ \cup \{0\}$
7		uncom	$⊢ ℕ \cup \{0\} = \{0\} \cup ℕ$
8		df-pr	$⊢ \{0, 1\} = \{0\} \cup \{1\}$
9	8	uneq1i	$⊢ \{0, 1\} \cup ℕ = (\{0\} \cup \{1\}) \cup ℕ$
10		unass	$⊢ (\{0\} \cup \{1\}) \cup ℕ = \{0\} \cup (\{1\} \cup ℕ)$
11		1nn	$⊢ 1 \in ℕ$
12		snssi	$⊢ 1 \in ℕ \to \{1\} \subseteq ℕ$
13	11 12	ax-mp	$⊢ \{1\} \subseteq ℕ$
14		ssequn1	$⊢ \{1\} \subseteq ℕ \leftrightarrow \{1\} \cup ℕ = ℕ$
15	13 14	mpbi	$⊢ \{1\} \cup ℕ = ℕ$
16	15	uneq2i	$⊢ \{0\} \cup (\{1\} \cup ℕ) = \{0\} \cup ℕ$
17	9 10 16	3eqtrri	$⊢ \{0\} \cup ℕ = \{0, 1\} \cup ℕ$
18	6 7 17	3eqtri	$⊢ ℕ_{0} = \{0, 1\} \cup ℕ$
19		oveq2	$⊢ k = i \to d ↑_{r} k = d ↑_{r} i$
20	19	cbviunv	$⊢ ⋃_{k \in \{0, 1\}} (d ↑_{r} k) = ⋃_{i \in \{0, 1\}} (d ↑_{r} i)$
21		ss2iun	$⊢ \forall i \in \{0, 1\} d ↑_{r} i \subseteq ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i \to ⋃_{i \in \{0, 1\}} (d ↑_{r} i) \subseteq ⋃_{i \in \{0, 1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
22		relexp1g	$⊢ d \in V \to d ↑_{r} 1 = d$
23	22	elv	$⊢ d ↑_{r} 1 = d$
24		oveq2	$⊢ j = 1 \to d ↑_{r} j = d ↑_{r} 1$
25	24	ssiun2s	$⊢ 1 \in ℕ \to d ↑_{r} 1 \subseteq ⋃_{j \in ℕ} (d ↑_{r} j)$
26	11 25	ax-mp	$⊢ d ↑_{r} 1 \subseteq ⋃_{j \in ℕ} (d ↑_{r} j)$
27	23 26	eqsstrri	$⊢ d \subseteq ⋃_{j \in ℕ} (d ↑_{r} j)$
28	27	a1i	$⊢ i \in \{0, 1\} \to d \subseteq ⋃_{j \in ℕ} (d ↑_{r} j)$
29		ovex	$⊢ d ↑_{r} j \in V$
30	5 29	iunex	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) \in V$
31	30	a1i	$⊢ i \in \{0, 1\} \to ⋃_{j \in ℕ} (d ↑_{r} j) \in V$
32		0nn0	$⊢ 0 \in ℕ_{0}$
33		1nn0	$⊢ 1 \in ℕ_{0}$
34		prssi	$⊢ (0 \in ℕ_{0} \land 1 \in ℕ_{0}) \to \{0, 1\} \subseteq ℕ_{0}$
35	32 33 34	mp2an	$⊢ \{0, 1\} \subseteq ℕ_{0}$
36	35	sseli	$⊢ i \in \{0, 1\} \to i \in ℕ_{0}$
37	28 31 36	relexpss1d	$⊢ i \in \{0, 1\} \to d ↑_{r} i \subseteq ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i$
38	21 37	mprg	$⊢ ⋃_{i \in \{0, 1\}} (d ↑_{r} i) \subseteq ⋃_{i \in \{0, 1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
39	20 38	eqsstri	$⊢ ⋃_{k \in \{0, 1\}} (d ↑_{r} k) \subseteq ⋃_{i \in \{0, 1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
40		oveq2	$⊢ k = j \to d ↑_{r} k = d ↑_{r} j$
41	40	cbviunv	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) = ⋃_{j \in ℕ} (d ↑_{r} j)$
42		relexp1g	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) \in V \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1 = ⋃_{j \in ℕ} (d ↑_{r} j)$
43	30 42	ax-mp	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1 = ⋃_{j \in ℕ} (d ↑_{r} j)$
44	41 43	eqtr4i	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1$
45		1ex	$⊢ 1 \in V$
46	45	prid2	$⊢ 1 \in \{0, 1\}$
47		oveq2	$⊢ i = 1 \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1$
48	47	ssiun2s	$⊢ 1 \in \{0, 1\} \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1 \subseteq ⋃_{i \in \{0, 1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
49	46 48	ax-mp	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1 \subseteq ⋃_{i \in \{0, 1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
50	44 49	eqsstri	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) \subseteq ⋃_{i \in \{0, 1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
51		c0ex	$⊢ 0 \in V$
52	51	prid1	$⊢ 0 \in \{0, 1\}$
53		oveq2	$⊢ k = 0 \to d ↑_{r} k = d ↑_{r} 0$
54	53	ssiun2s	$⊢ 0 \in \{0, 1\} \to d ↑_{r} 0 \subseteq ⋃_{k \in \{0, 1\}} (d ↑_{r} k)$
55	52 54	ax-mp	$⊢ d ↑_{r} 0 \subseteq ⋃_{k \in \{0, 1\}} (d ↑_{r} k)$
56		ssid	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)$
57		unss12	$⊢ (d ↑_{r} 0 \subseteq ⋃_{k \in \{0, 1\}} (d ↑_{r} k) \land ⋃_{k \in ℕ} (d ↑_{r} k) \subseteq ⋃_{k \in ℕ} (d ↑_{r} k)) \to (d ↑_{r} 0) \cup ⋃_{k \in ℕ} (d ↑_{r} k) \subseteq ⋃_{k \in \{0, 1\}} (d ↑_{r} k) \cup ⋃_{k \in ℕ} (d ↑_{r} k)$
58	55 56 57	mp2an	$⊢ (d ↑_{r} 0) \cup ⋃_{k \in ℕ} (d ↑_{r} k) \subseteq ⋃_{k \in \{0, 1\}} (d ↑_{r} k) \cup ⋃_{k \in ℕ} (d ↑_{r} k)$
59		iuneq1	$⊢ \{0, 1\} = \{0\} \cup \{1\} \to ⋃_{i \in \{0, 1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = ⋃_{i \in \{0\} \cup \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
60	8 59	ax-mp	$⊢ ⋃_{i \in \{0, 1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = ⋃_{i \in \{0\} \cup \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
61		iunxun	$⊢ ⋃_{i \in \{0\} \cup \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = ⋃_{i \in \{0\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) \cup ⋃_{i \in \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i)$
62		oveq2	$⊢ i = 0 \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 0$
63	51 62	iunxsn	$⊢ ⋃_{i \in \{0\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 0$
64		vex	$⊢ d \in V$
65		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
66		inelcm	$⊢ (1 \in \{0, 1\} \land 1 \in ℕ) \to \{0, 1\} \cap ℕ \neq \emptyset$
67	46 11 66	mp2an	$⊢ \{0, 1\} \cap ℕ \neq \emptyset$
68		iunrelexp0	$⊢ (d \in V \land ℕ \subseteq ℕ_{0} \land \{0, 1\} \cap ℕ \neq \emptyset) \to ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 0 = d ↑_{r} 0$
69	64 65 67 68	mp3an	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 0 = d ↑_{r} 0$
70	63 69	eqtri	$⊢ ⋃_{i \in \{0\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = d ↑_{r} 0$
71	45 47	iunxsn	$⊢ ⋃_{i \in \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1$
72	43 41	eqtr4i	$⊢ ⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} 1 = ⋃_{k \in ℕ} (d ↑_{r} k)$
73	71 72	eqtri	$⊢ ⋃_{i \in \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = ⋃_{k \in ℕ} (d ↑_{r} k)$
74	70 73	uneq12i	$⊢ ⋃_{i \in \{0\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) \cup ⋃_{i \in \{1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = (d ↑_{r} 0) \cup ⋃_{k \in ℕ} (d ↑_{r} k)$
75	60 61 74	3eqtri	$⊢ ⋃_{i \in \{0, 1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) = (d ↑_{r} 0) \cup ⋃_{k \in ℕ} (d ↑_{r} k)$
76		iunxun	$⊢ ⋃_{k \in \{0, 1\} \cup ℕ} (d ↑_{r} k) = ⋃_{k \in \{0, 1\}} (d ↑_{r} k) \cup ⋃_{k \in ℕ} (d ↑_{r} k)$
77	58 75 76	3sstr4i	$⊢ ⋃_{i \in \{0, 1\}} (⋃_{j \in ℕ} (d ↑_{r} j) ↑_{r} i) \subseteq ⋃_{k \in \{0, 1\} \cup ℕ} (d ↑_{r} k)$
78	1 2 3 4 5 18 39 50 77	comptiunov2i	$⊢ r* \circ t+ = t*$

Metamath Proof Explorer

Theorem corcltrcl

Proof