trclimalb2

Description: Lower bound for image under a transitive closure. (Contributed by RP, 1-Jul-2020)

		Ref	Expression
	Assertion	trclimalb2	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to t+ (R) [A] \subseteq B$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ R \in V \to R \in V$
2	1	adantr	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to R \in V$
3		oveq1	$⊢ r = R \to r ↑_{r} k = R ↑_{r} k$
4	3	iuneq2d	$⊢ r = R \to ⋃_{k \in ℕ} (r ↑_{r} k) = ⋃_{k \in ℕ} (R ↑_{r} k)$
5		dftrcl3	$⊢ t+ = (r \in V ⟼ ⋃_{k \in ℕ} (r ↑_{r} k))$
6		nnex	$⊢ ℕ \in V$
7		ovex	$⊢ R ↑_{r} k \in V$
8	6 7	iunex	$⊢ ⋃_{k \in ℕ} (R ↑_{r} k) \in V$
9	4 5 8	fvmpt	$⊢ R \in V \to t+ (R) = ⋃_{k \in ℕ} (R ↑_{r} k)$
10	9	imaeq1d	$⊢ R \in V \to t+ (R) [A] = ⋃_{k \in ℕ} (R ↑_{r} k) [A]$
11		imaiun1	$⊢ ⋃_{k \in ℕ} (R ↑_{r} k) [A] = ⋃_{k \in ℕ} (R ↑_{r} k) [A]$
12	10 11	eqtrdi	$⊢ R \in V \to t+ (R) [A] = ⋃_{k \in ℕ} (R ↑_{r} k) [A]$
13	2 12	syl	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to t+ (R) [A] = ⋃_{k \in ℕ} (R ↑_{r} k) [A]$
14		oveq2	$⊢ x = 1 \to R ↑_{r} x = R ↑_{r} 1$
15	14	imaeq1d	$⊢ x = 1 \to (R ↑_{r} x) [A] = (R ↑_{r} 1) [A]$
16	15	sseq1d	$⊢ x = 1 \to ((R ↑_{r} x) [A] \subseteq B \leftrightarrow (R ↑_{r} 1) [A] \subseteq B)$
17	16	imbi2d	$⊢ x = 1 \to (((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} x) [A] \subseteq B) \leftrightarrow ((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} 1) [A] \subseteq B))$
18		oveq2	$⊢ x = y \to R ↑_{r} x = R ↑_{r} y$
19	18	imaeq1d	$⊢ x = y \to (R ↑_{r} x) [A] = (R ↑_{r} y) [A]$
20	19	sseq1d	$⊢ x = y \to ((R ↑_{r} x) [A] \subseteq B \leftrightarrow (R ↑_{r} y) [A] \subseteq B)$
21	20	imbi2d	$⊢ x = y \to (((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} x) [A] \subseteq B) \leftrightarrow ((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} y) [A] \subseteq B))$
22		oveq2	$⊢ x = y + 1 \to R ↑_{r} x = R ↑_{r} (y + 1)$
23	22	imaeq1d	$⊢ x = y + 1 \to (R ↑_{r} x) [A] = (R ↑_{r} (y + 1)) [A]$
24	23	sseq1d	$⊢ x = y + 1 \to ((R ↑_{r} x) [A] \subseteq B \leftrightarrow (R ↑_{r} (y + 1)) [A] \subseteq B)$
25	24	imbi2d	$⊢ x = y + 1 \to (((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} x) [A] \subseteq B) \leftrightarrow ((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} (y + 1)) [A] \subseteq B))$
26		oveq2	$⊢ x = k \to R ↑_{r} x = R ↑_{r} k$
27	26	imaeq1d	$⊢ x = k \to (R ↑_{r} x) [A] = (R ↑_{r} k) [A]$
28	27	sseq1d	$⊢ x = k \to ((R ↑_{r} x) [A] \subseteq B \leftrightarrow (R ↑_{r} k) [A] \subseteq B)$
29	28	imbi2d	$⊢ x = k \to (((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} x) [A] \subseteq B) \leftrightarrow ((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} k) [A] \subseteq B))$
30		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
31	30	imaeq1d	$⊢ R \in V \to (R ↑_{r} 1) [A] = R [A]$
32	31	adantr	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} 1) [A] = R [A]$
33		ssun1	$⊢ A \subseteq A \cup B$
34		imass2	$⊢ A \subseteq A \cup B \to R [A] \subseteq R [A \cup B]$
35	33 34	mp1i	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to R [A] \subseteq R [A \cup B]$
36		simpr	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to R [A \cup B] \subseteq B$
37	35 36	sstrd	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to R [A] \subseteq B$
38	32 37	eqsstrd	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} 1) [A] \subseteq B$
39		simp2l	$⊢ (y \in ℕ \land (R \in V \land R [A \cup B] \subseteq B) \land (R ↑_{r} y) [A] \subseteq B) \to R \in V$
40		simp1	$⊢ (y \in ℕ \land (R \in V \land R [A \cup B] \subseteq B) \land (R ↑_{r} y) [A] \subseteq B) \to y \in ℕ$
41		relexpsucnnl	$⊢ (R \in V \land y \in ℕ) \to R ↑_{r} (y + 1) = R \circ (R ↑_{r} y)$
42	41	imaeq1d	$⊢ (R \in V \land y \in ℕ) \to (R ↑_{r} (y + 1)) [A] = (R \circ (R ↑_{r} y)) [A]$
43		imaco	$⊢ (R \circ (R ↑_{r} y)) [A] = R [(R ↑_{r} y) [A]]$
44	42 43	eqtrdi	$⊢ (R \in V \land y \in ℕ) \to (R ↑_{r} (y + 1)) [A] = R [(R ↑_{r} y) [A]]$
45	39 40 44	syl2anc	$⊢ (y \in ℕ \land (R \in V \land R [A \cup B] \subseteq B) \land (R ↑_{r} y) [A] \subseteq B) \to (R ↑_{r} (y + 1)) [A] = R [(R ↑_{r} y) [A]]$
46		imass2	$⊢ (R ↑_{r} y) [A] \subseteq B \to R [(R ↑_{r} y) [A]] \subseteq R [B]$
47	46	3ad2ant3	$⊢ (y \in ℕ \land (R \in V \land R [A \cup B] \subseteq B) \land (R ↑_{r} y) [A] \subseteq B) \to R [(R ↑_{r} y) [A]] \subseteq R [B]$
48		ssun2	$⊢ B \subseteq A \cup B$
49		imass2	$⊢ B \subseteq A \cup B \to R [B] \subseteq R [A \cup B]$
50	48 49	mp1i	$⊢ (y \in ℕ \land (R \in V \land R [A \cup B] \subseteq B) \land (R ↑_{r} y) [A] \subseteq B) \to R [B] \subseteq R [A \cup B]$
51		simp2r	$⊢ (y \in ℕ \land (R \in V \land R [A \cup B] \subseteq B) \land (R ↑_{r} y) [A] \subseteq B) \to R [A \cup B] \subseteq B$
52	50 51	sstrd	$⊢ (y \in ℕ \land (R \in V \land R [A \cup B] \subseteq B) \land (R ↑_{r} y) [A] \subseteq B) \to R [B] \subseteq B$
53	47 52	sstrd	$⊢ (y \in ℕ \land (R \in V \land R [A \cup B] \subseteq B) \land (R ↑_{r} y) [A] \subseteq B) \to R [(R ↑_{r} y) [A]] \subseteq B$
54	45 53	eqsstrd	$⊢ (y \in ℕ \land (R \in V \land R [A \cup B] \subseteq B) \land (R ↑_{r} y) [A] \subseteq B) \to (R ↑_{r} (y + 1)) [A] \subseteq B$
55	54	3exp	$⊢ y \in ℕ \to ((R \in V \land R [A \cup B] \subseteq B) \to ((R ↑_{r} y) [A] \subseteq B \to (R ↑_{r} (y + 1)) [A] \subseteq B))$
56	55	a2d	$⊢ y \in ℕ \to (((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} y) [A] \subseteq B) \to ((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} (y + 1)) [A] \subseteq B))$
57	17 21 25 29 38 56	nnind	$⊢ k \in ℕ \to ((R \in V \land R [A \cup B] \subseteq B) \to (R ↑_{r} k) [A] \subseteq B)$
58	57	com12	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to (k \in ℕ \to (R ↑_{r} k) [A] \subseteq B)$
59	58	ralrimiv	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to \forall k \in ℕ (R ↑_{r} k) [A] \subseteq B$
60		iunss	$⊢ ⋃_{k \in ℕ} (R ↑_{r} k) [A] \subseteq B \leftrightarrow \forall k \in ℕ (R ↑_{r} k) [A] \subseteq B$
61	59 60	sylibr	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to ⋃_{k \in ℕ} (R ↑_{r} k) [A] \subseteq B$
62	13 61	eqsstrd	$⊢ (R \in V \land R [A \cup B] \subseteq B) \to t+ (R) [A] \subseteq B$

Metamath Proof Explorer

Theorem trclimalb2

Proof