Metamath Proof Explorer

Theorem trclimalb2

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

Ref Expression
Assertion trclimalb2 ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( t+ ‘ 𝑅 ) “ 𝐴 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
2 1 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → 𝑅 ∈ V )
3 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑𝑟 𝑘 ) = ( 𝑅 ↑𝑟 𝑘 ) )
4 3 iuneq2d ⊢ ( 𝑟 = 𝑅 → ∪ 𝑘 ∈ ℕ ( 𝑟 ↑𝑟 𝑘 ) = ∪ 𝑘 ∈ ℕ ( 𝑅 ↑𝑟 𝑘 ) )
5 dftrcl3 ⊢ t+ = ( 𝑟 ∈ V ↦ ∪ 𝑘 ∈ ℕ ( 𝑟 ↑𝑟 𝑘 ) )
6 nnex ⊢ ℕ ∈ V
7 ovex ⊢ ( 𝑅 ↑𝑟 𝑘 ) ∈ V
8 6 7 iunex ⊢ ∪ 𝑘 ∈ ℕ ( 𝑅 ↑𝑟 𝑘 ) ∈ V
9 4 5 8 fvmpt ⊢ ( 𝑅 ∈ V → ( t+ ‘ 𝑅 ) = ∪ 𝑘 ∈ ℕ ( 𝑅 ↑𝑟 𝑘 ) )
10 9 imaeq1d ⊢ ( 𝑅 ∈ V → ( ( t+ ‘ 𝑅 ) “ 𝐴 ) = ( ∪ 𝑘 ∈ ℕ ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) )
11 imaiun1 ⊢ ( ∪ 𝑘 ∈ ℕ ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) = ∪ 𝑘 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 )
12 10 11 eqtrdi ⊢ ( 𝑅 ∈ V → ( ( t+ ‘ 𝑅 ) “ 𝐴 ) = ∪ 𝑘 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) )
13 2 12 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( t+ ‘ 𝑅 ) “ 𝐴 ) = ∪ 𝑘 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) )
14 oveq2 ⊢ ( 𝑥 = 1 → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 1 ) )
15 14 imaeq1d ⊢ ( 𝑥 = 1 → ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) = ( ( 𝑅 ↑𝑟 1 ) “ 𝐴 ) )
16 15 sseq1d ⊢ ( 𝑥 = 1 → ( ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) ⊆ 𝐵 ↔ ( ( 𝑅 ↑𝑟 1 ) “ 𝐴 ) ⊆ 𝐵 ) )
17 16 imbi2d ⊢ ( 𝑥 = 1 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) ⊆ 𝐵 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 1 ) “ 𝐴 ) ⊆ 𝐵 ) ) )
18 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 𝑦 ) )
19 18 imaeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) = ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) )
20 19 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) ⊆ 𝐵 ↔ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) )
21 20 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) ⊆ 𝐵 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) ) )
22 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) )
23 22 imaeq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) = ( ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) “ 𝐴 ) )
24 23 sseq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) ⊆ 𝐵 ↔ ( ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) “ 𝐴 ) ⊆ 𝐵 ) )
25 24 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) ⊆ 𝐵 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) “ 𝐴 ) ⊆ 𝐵 ) ) )
26 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 𝑘 ) )
27 26 imaeq1d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) = ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) )
28 27 sseq1d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) ⊆ 𝐵 ↔ ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) ⊆ 𝐵 ) )
29 28 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 𝑥 ) “ 𝐴 ) ⊆ 𝐵 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) ⊆ 𝐵 ) ) )
30 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
31 30 imaeq1d ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 1 ) “ 𝐴 ) = ( 𝑅 “ 𝐴 ) )
32 31 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 1 ) “ 𝐴 ) = ( 𝑅 “ 𝐴 ) )
33 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
34 imass2 ⊢ ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) → ( 𝑅 “ 𝐴 ) ⊆ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) )
35 33 34 mp1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( 𝑅 “ 𝐴 ) ⊆ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) )
36 simpr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 )
37 35 36 sstrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( 𝑅 “ 𝐴 ) ⊆ 𝐵 )
38 32 37 eqsstrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 1 ) “ 𝐴 ) ⊆ 𝐵 )
39 simp2l ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) ∧ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) → 𝑅 ∈ 𝑉 )
40 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) ∧ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) → 𝑦 ∈ ℕ )
41 relexpsucnnl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑦 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑦 ) ) )
42 41 imaeq1d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑦 ∈ ℕ ) → ( ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) “ 𝐴 ) = ( ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑦 ) ) “ 𝐴 ) )
43 imaco ⊢ ( ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑦 ) ) “ 𝐴 ) = ( 𝑅 “ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) )
44 42 43 eqtrdi ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑦 ∈ ℕ ) → ( ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) “ 𝐴 ) = ( 𝑅 “ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ) )
45 39 40 44 syl2anc ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) ∧ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) “ 𝐴 ) = ( 𝑅 “ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ) )
46 imass2 ⊢ ( ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 → ( 𝑅 “ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ) ⊆ ( 𝑅 “ 𝐵 ) )
47 46 3ad2ant3 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) ∧ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) → ( 𝑅 “ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ) ⊆ ( 𝑅 “ 𝐵 ) )
48 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
49 imass2 ⊢ ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) → ( 𝑅 “ 𝐵 ) ⊆ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) )
50 48 49 mp1i ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) ∧ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) → ( 𝑅 “ 𝐵 ) ⊆ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) )
51 simp2r ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) ∧ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) → ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 )
52 50 51 sstrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) ∧ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) → ( 𝑅 “ 𝐵 ) ⊆ 𝐵 )
53 47 52 sstrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) ∧ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) → ( 𝑅 “ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ) ⊆ 𝐵 )
54 45 53 eqsstrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) ∧ ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) “ 𝐴 ) ⊆ 𝐵 )
55 54 3exp ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 → ( ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) “ 𝐴 ) ⊆ 𝐵 ) ) )
56 55 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 𝑦 ) “ 𝐴 ) ⊆ 𝐵 ) → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) “ 𝐴 ) ⊆ 𝐵 ) ) )
57 17 21 25 29 38 56 nnind ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) ⊆ 𝐵 ) )
58 57 com12 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( 𝑘 ∈ ℕ → ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) ⊆ 𝐵 ) )
59 58 ralrimiv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ∀ 𝑘 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) ⊆ 𝐵 )
60 iunss ⊢ ( ∪ 𝑘 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑘 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) ⊆ 𝐵 )
61 59 60 sylibr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ∪ 𝑘 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑘 ) “ 𝐴 ) ⊆ 𝐵 )
62 13 61 eqsstrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑅 “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝐵 ) → ( ( t+ ‘ 𝑅 ) “ 𝐴 ) ⊆ 𝐵 )