iunrelexpmin2

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

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

Proof

Step	Hyp	Ref	Expression
1		iunrelexpmin2.def	$⊢ C = (r \in V ⟼ ⋃_{n \in N} (r ↑_{r} n))$
2		simplr	$⊢ ((R \in V \land N = ℕ_{0}) \land r = R) \to N = ℕ_{0}$
3		simpr	$⊢ ((R \in V \land N = ℕ_{0}) \land r = R) \to r = R$
4	3	oveq1d	$⊢ ((R \in V \land N = ℕ_{0}) \land r = R) \to r ↑_{r} n = R ↑_{r} n$
5	2 4	iuneq12d	$⊢ ((R \in V \land N = ℕ_{0}) \land r = R) \to ⋃_{n \in N} (r ↑_{r} n) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
6		elex	$⊢ R \in V \to R \in V$
7	6	adantr	$⊢ (R \in V \land N = ℕ_{0}) \to R \in V$
8		nn0ex	$⊢ ℕ_{0} \in V$
9		ovex	$⊢ R ↑_{r} n \in V$
10	8 9	iunex	$⊢ ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \in V$
11	10	a1i	$⊢ (R \in V \land N = ℕ_{0}) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \in V$
12	1 5 7 11	fvmptd2	$⊢ (R \in V \land N = ℕ_{0}) \to C (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
13		relexp0g	$⊢ R \in V \to R ↑_{r} 0 = {I ↾}_{(dom R \cup ran R)}$
14	13	sseq1d	$⊢ R \in V \to (R ↑_{r} 0 \subseteq s \leftrightarrow {I ↾}_{(dom R \cup ran R)} \subseteq s)$
15		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
16	15	sseq1d	$⊢ R \in V \to (R ↑_{r} 1 \subseteq s \leftrightarrow R \subseteq s)$
17	14 16	3anbi12d	$⊢ R \in V \to ((R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s) \leftrightarrow ({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s))$
18		elnn0	$⊢ n \in ℕ_{0} \leftrightarrow (n \in ℕ \lor n = 0)$
19		oveq2	$⊢ x = 1 \to R ↑_{r} x = R ↑_{r} 1$
20	19	sseq1d	$⊢ x = 1 \to (R ↑_{r} x \subseteq s \leftrightarrow R ↑_{r} 1 \subseteq s)$
21	20	imbi2d	$⊢ x = 1 \to (((R \in V \land (R ↑_{r} 0 \subseteq s \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} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} 1 \subseteq s))$
22		oveq2	$⊢ x = y \to R ↑_{r} x = R ↑_{r} y$
23	22	sseq1d	$⊢ x = y \to (R ↑_{r} x \subseteq s \leftrightarrow R ↑_{r} y \subseteq s)$
24	23	imbi2d	$⊢ x = y \to (((R \in V \land (R ↑_{r} 0 \subseteq s \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} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} y \subseteq s))$
25		oveq2	$⊢ x = y + 1 \to R ↑_{r} x = R ↑_{r} (y + 1)$
26	25	sseq1d	$⊢ x = y + 1 \to (R ↑_{r} x \subseteq s \leftrightarrow R ↑_{r} (y + 1) \subseteq s)$
27	26	imbi2d	$⊢ x = y + 1 \to (((R \in V \land (R ↑_{r} 0 \subseteq s \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} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} (y + 1) \subseteq s))$
28		oveq2	$⊢ x = n \to R ↑_{r} x = R ↑_{r} n$
29	28	sseq1d	$⊢ x = n \to (R ↑_{r} x \subseteq s \leftrightarrow R ↑_{r} n \subseteq s)$
30	29	imbi2d	$⊢ x = n \to (((R \in V \land (R ↑_{r} 0 \subseteq s \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} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} n \subseteq s))$
31		simpr2	$⊢ (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} 1 \subseteq s$
32		simp1	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to y \in ℕ$
33		1nn	$⊢ 1 \in ℕ$
34	33	a1i	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to 1 \in ℕ$
35		simp2l	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to R \in V$
36		relexpaddnn	$⊢ (y \in ℕ \land 1 \in ℕ \land R \in V) \to (R ↑_{r} y) \circ (R ↑_{r} 1) = R ↑_{r} (y + 1)$
37	32 34 35 36	syl3anc	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 0 \subseteq s \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)$
38		simp2r3	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to s \circ s \subseteq s$
39		simp3	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to R ↑_{r} y \subseteq s$
40		simp2r2	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \land R ↑_{r} y \subseteq s) \to R ↑_{r} 1 \subseteq s$
41	38 39 40	trrelssd	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 0 \subseteq s \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$
42	37 41	eqsstrrd	$⊢ (y \in ℕ \land (R \in V \land (R ↑_{r} 0 \subseteq s \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$
43	42	3exp	$⊢ y \in ℕ \to ((R \in V \land (R ↑_{r} 0 \subseteq s \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))$
44	43	a2d	$⊢ y \in ℕ \to (((R \in V \land (R ↑_{r} 0 \subseteq s \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} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} (y + 1) \subseteq s))$
45	21 24 27 30 31 44	nnind	$⊢ n \in ℕ \to ((R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} n \subseteq s)$
46		simpr1	$⊢ (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} 0 \subseteq s$
47		oveq2	$⊢ n = 0 \to R ↑_{r} n = R ↑_{r} 0$
48	47	sseq1d	$⊢ n = 0 \to (R ↑_{r} n \subseteq s \leftrightarrow R ↑_{r} 0 \subseteq s)$
49	46 48	syl5ibr	$⊢ n = 0 \to ((R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} n \subseteq s)$
50	45 49	jaoi	$⊢ (n \in ℕ \lor n = 0) \to ((R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} n \subseteq s)$
51	18 50	sylbi	$⊢ n \in ℕ_{0} \to ((R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to R ↑_{r} n \subseteq s)$
52	51	com12	$⊢ (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to (n \in ℕ_{0} \to R ↑_{r} n \subseteq s)$
53	52	ralrimiv	$⊢ (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to \forall n \in ℕ_{0} R ↑_{r} n \subseteq s$
54		iunss	$⊢ ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s \leftrightarrow \forall n \in ℕ_{0} R ↑_{r} n \subseteq s$
55	53 54	sylibr	$⊢ (R \in V \land (R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s)) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s$
56	55	ex	$⊢ R \in V \to ((R ↑_{r} 0 \subseteq s \land R ↑_{r} 1 \subseteq s \land s \circ s \subseteq s) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s)$
57	17 56	sylbird	$⊢ R \in V \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s)$
58	57	adantr	$⊢ (R \in V \land N = ℕ_{0}) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s)$
59		sseq1	$⊢ C (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \to (C (R) \subseteq s \leftrightarrow ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s)$
60	59	imbi2d	$⊢ C (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \to ((({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to C (R) \subseteq s) \leftrightarrow (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s))$
61	58 60	syl5ibr	$⊢ C (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \to ((R \in V \land N = ℕ_{0}) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to C (R) \subseteq s))$
62	12 61	mpcom	$⊢ (R \in V \land N = ℕ_{0}) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to C (R) \subseteq s)$
63	62	alrimiv	$⊢ (R \in V \land N = ℕ_{0}) \to \forall s (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to C (R) \subseteq s)$

Metamath Proof Explorer

Theorem iunrelexpmin2

Proof