rtrclreclem2

Description: The reflexive, transitive closure is indeed reflexive. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 13-Jul-2024)

	Ref	Expression
Hypotheses	rtrclreclem2.1	$⊢ φ \to Rel R$
	rtrclreclem2.2	$⊢ φ \to R \in V$
Assertion	rtrclreclem2	$⊢ φ \to {I ↾}_{⋃ ⋃ R} \subseteq t*rec (R)$

Proof

Step	Hyp	Ref	Expression
1		rtrclreclem2.1	$⊢ φ \to Rel R$
2		rtrclreclem2.2	$⊢ φ \to R \in V$
3		0nn0	$⊢ 0 \in ℕ_{0}$
4		ssid	$⊢ {I ↾}_{⋃ ⋃ R} \subseteq {I ↾}_{⋃ ⋃ R}$
5	1 2	relexp0d	$⊢ φ \to R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R}$
6	4 5	sseqtrrid	$⊢ φ \to {I ↾}_{⋃ ⋃ R} \subseteq R ↑_{r} 0$
7		oveq2	$⊢ n = 0 \to R ↑_{r} n = R ↑_{r} 0$
8	7	sseq2d	$⊢ n = 0 \to ({I ↾}_{⋃ ⋃ R} \subseteq R ↑_{r} n \leftrightarrow {I ↾}_{⋃ ⋃ R} \subseteq R ↑_{r} 0)$
9	8	rspcev	$⊢ (0 \in ℕ_{0} \land {I ↾}_{⋃ ⋃ R} \subseteq R ↑_{r} 0) \to \exists n \in ℕ_{0} {I ↾}_{⋃ ⋃ R} \subseteq R ↑_{r} n$
10	3 6 9	sylancr	$⊢ φ \to \exists n \in ℕ_{0} {I ↾}_{⋃ ⋃ R} \subseteq R ↑_{r} n$
11		ssiun	$⊢ \exists n \in ℕ_{0} {I ↾}_{⋃ ⋃ R} \subseteq R ↑_{r} n \to {I ↾}_{⋃ ⋃ R} \subseteq ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
12	10 11	syl	$⊢ φ \to {I ↾}_{⋃ ⋃ R} \subseteq ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
13	2	elexd	$⊢ φ \to R \in V$
14		nn0ex	$⊢ ℕ_{0} \in V$
15		ovex	$⊢ R ↑_{r} n \in V$
16	14 15	iunex	$⊢ ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \in V$
17		oveq1	$⊢ r = R \to r ↑_{r} n = R ↑_{r} n$
18	17	iuneq2d	$⊢ r = R \to ⋃_{n \in ℕ_{0}} (r ↑_{r} n) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
19		eqid	$⊢ (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n))$
20	18 19	fvmptg	$⊢ (R \in V \land ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \in V) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
21	13 16 20	sylancl	$⊢ φ \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
22	12 21	sseqtrrd	$⊢ φ \to {I ↾}_{⋃ ⋃ R} \subseteq (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R)$
23		df-rtrclrec	$⊢ t*rec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n))$
24		fveq1	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to trec (R) = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R)$
25	24	sseq2d	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to ({I ↾}_{⋃ ⋃ R} \subseteq trec (R) \leftrightarrow {I ↾}_{⋃ ⋃ R} \subseteq (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R))$
26	25	imbi2d	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to ((φ \to {I ↾}_{⋃ ⋃ R} \subseteq trec (R)) \leftrightarrow (φ \to {I ↾}_{⋃ ⋃ R} \subseteq (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R)))$
27	23 26	ax-mp	$⊢ (φ \to {I ↾}_{⋃ ⋃ R} \subseteq t*rec (R)) \leftrightarrow (φ \to {I ↾}_{⋃ ⋃ R} \subseteq (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R))$
28	22 27	mpbir	$⊢ φ \to {I ↾}_{⋃ ⋃ R} \subseteq t*rec (R)$

Metamath Proof Explorer

Theorem rtrclreclem2

Proof