iunrelexpmin1

Description: The indexed union of relation exponentiation over the natural numbers is the minimum transitive relation that includes the relation. (Contributed by RP, 4-Jun-2020)

		Ref	Expression
	Hypothesis	iunrelexpmin1.def	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r ↑_{r} n))$
	Assertion	iunrelexpmin1	$⊢ (R \in V \land N = ℕ) \to \forall s ((R \subseteq s \land s \circ s \subseteq s) \to C (R) \subseteq s)$

Proof

Step	Hyp	Ref	Expression
1		iunrelexpmin1.def	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r ↑_{r} n))$
2		simplr	$⊢ ((R \in V \land N = ℕ) \land r = R) \to N = ℕ$
3		simpr	$⊢ ((R \in V \land N = ℕ) \land r = R) \to r = R$
4	3	oveq1d	$⊢ ((R \in V \land N = ℕ) \land r = R) \to r ↑_{r} n = R ↑_{r} n$
5	2 4	iuneq12d	$⊢ ((R \in V \land N = ℕ) \land r = R) \to ⋃_{n \in N} (r ↑_{r} n) = ⋃_{n \in ℕ} (R ↑_{r} n)$
6		elex	$⊢ R \in V \to R \in V$
7	6	adantr	$⊢ (R \in V \land N = ℕ) \to R \in V$
8		nnex	$⊢ ℕ \in V$
9		ovex	$⊢ R ↑_{r} n \in V$
10	8 9	iunex	$⊢ ⋃_{n \in ℕ} (R ↑_{r} n) \in V$
11	10	a1i	$⊢ (R \in V \land N = ℕ) \to ⋃_{n \in ℕ} (R ↑_{r} n) \in V$
12	1 5 7 11	fvmptd2	$⊢ (R \in V \land N = ℕ) \to C (R) = ⋃_{n \in ℕ} (R ↑_{r} n)$
13		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
14	13	sseq1d	$⊢ R \in V \to (R ↑_{r} 1 \subseteq s \leftrightarrow R \subseteq s)$
15	14	anbi1d	$⊢ R \in V \to ((R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s) \leftrightarrow (R \subseteq s \land s \circ s \subseteq s))$
16		oveq2	$⊢ x = 1 \to R ↑_{r} x = R ↑_{r} 1$
17	16	sseq1d	$⊢ x = 1 \to (R ↑_{r} x \subseteq s \leftrightarrow R ↑_{r} 1 \subseteq s)$
18	17	imbi2d	$⊢ x = 1 \to (((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} x \subseteq s) \leftrightarrow ((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} 1 \subseteq s))$
19		oveq2	$⊢ x = y \to R ↑_{r} x = R ↑_{r} y$
20	19	sseq1d	$⊢ x = y \to (R ↑_{r} x \subseteq s \leftrightarrow R ↑_{r} y \subseteq s)$
21	20	imbi2d	$⊢ x = y \to (((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} x \subseteq s) \leftrightarrow ((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} y \subseteq s))$
22		oveq2	$⊢ x = y + 1 \to R ↑_{r} x = R ↑_{r} (y + 1)$
23	22	sseq1d	$⊢ x = y + 1 \to (R ↑_{r} x \subseteq s \leftrightarrow R ↑_{r} (y + 1) \subseteq s)$
24	23	imbi2d	$⊢ x = y + 1 \to (((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} x \subseteq s) \leftrightarrow ((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} (y + 1) \subseteq s))$
25		oveq2	$⊢ x = n \to R ↑_{r} x = R ↑_{r} n$
26	25	sseq1d	$⊢ x = n \to (R ↑_{r} x \subseteq s \leftrightarrow R ↑_{r} n \subseteq s)$
27	26	imbi2d	$⊢ x = n \to (((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} x \subseteq s) \leftrightarrow ((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} n \subseteq s))$
28		simprl	$⊢ (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} 1 \subseteq s$
29		simp1	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to y \in ℕ$
30		1nn	$⊢ 1 \in ℕ$
31	30	a1i	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to 1 \in ℕ$
32		simp2l	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to R \in V$
33		relexpaddnn	$⊢ (y \in ℕ \land 1 \in ℕ \land R \in V) \to (R ↑_{r} y) \circ (R ↑_{r} 1) = R ↑_{r} (y + 1)$
34	29 31 32 33	syl3anc	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to (R ↑_{r} y) \circ (R ↑_{r} 1) = R ↑_{r} (y + 1)$
35		simp2rr	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to s \circ s \subseteq s$
36		simp3	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to R ↑_{r} y \subseteq s$
37		simp2rl	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to R ↑_{r} 1 \subseteq s$
38	35 36 37	trrelssd	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to (R ↑_{r} y) \circ (R ↑_{r} 1) \subseteq s$
39	34 38	eqsstrrd	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to R ↑_{r} (y + 1) \subseteq s$
40	39	3exp	$⊢ y \in ℕ \to ((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to (R ↑_{r} y \subseteq s \to R ↑_{r} (y + 1) \subseteq s))$
41	40	a2d	$⊢ y \in ℕ \to (((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} y \subseteq s) \to ((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} (y + 1) \subseteq s))$
42	18 21 24 27 28 41	nnind	$⊢ n \in ℕ \to ((R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} n \subseteq s)$
43	42	com12	$⊢ (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to (n \in ℕ \to R ↑_{r} n \subseteq s)$
44	43	ralrimiv	$⊢ (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to \forall n \in ℕ R ↑_{r} n \subseteq s$
45		iunss	$⊢ ⋃_{n \in ℕ} (R ↑_{r} n) \subseteq s \leftrightarrow \forall n \in ℕ R ↑_{r} n \subseteq s$
46	44 45	sylibr	$⊢ (R \in V \land (R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to ⋃_{n \in ℕ} (R ↑_{r} n) \subseteq s$
47	46	ex	$⊢ R \in V \to ((R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s) \to ⋃_{n \in ℕ} (R ↑_{r} n) \subseteq s)$
48	15 47	sylbird	$⊢ R \in V \to ((R \subseteq s \land s \circ s \subseteq s) \to ⋃_{n \in ℕ} (R ↑_{r} n) \subseteq s)$
49	48	adantr	$⊢ (R \in V \land N = ℕ) \to ((R \subseteq s \land s \circ s \subseteq s) \to ⋃_{n \in ℕ} (R ↑_{r} n) \subseteq s)$
50		sseq1	$⊢ C (R) = ⋃_{n \in ℕ} (R ↑_{r} n) \to (C (R) \subseteq s \leftrightarrow ⋃_{n \in ℕ} (R ↑_{r} n) \subseteq s)$
51	50	imbi2d	$⊢ C (R) = ⋃_{n \in ℕ} (R ↑_{r} n) \to (((R \subseteq s \land s \circ s \subseteq s) \to C (R) \subseteq s) \leftrightarrow ((R \subseteq s \land s \circ s \subseteq s) \to ⋃_{n \in ℕ} (R ↑_{r} n) \subseteq s))$
52	49 51	syl5ibr	$⊢ C (R) = ⋃_{n \in ℕ} (R ↑_{r} n) \to ((R \in V \land N = ℕ) \to ((R \subseteq s \land s \circ s \subseteq s) \to C (R) \subseteq s))$
53	12 52	mpcom	$⊢ (R \in V \land N = ℕ) \to ((R \subseteq s \land s \circ s \subseteq s) \to C (R) \subseteq s)$
54	53	alrimiv	$⊢ (R \in V \land N = ℕ) \to \forall s ((R \subseteq s \land s \circ s \subseteq s) \to C (R) \subseteq s)$

Metamath Proof Explorer

Theorem iunrelexpmin1

Proof