Metamath Proof Explorer

Theorem 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 ⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
Assertion iunrelexpmin1 ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) → ∀ 𝑠 ( ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ) )

Proof

Step Hyp Ref Expression
1 iunrelexpmin1.def ⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) )
2 simplr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) ∧ 𝑟 = 𝑅 ) → 𝑁 = ℕ )
3 simpr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
4 3 oveq1d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) ∧ 𝑟 = 𝑅 ) → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑛 ) )
5 2 4 iuneq12d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) ∧ 𝑟 = 𝑅 ) → ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) )
6 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
7 6 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) → 𝑅 ∈ V )
8 nnex ⊢ ℕ ∈ V
9 ovex ⊢ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
10 8 9 iunex ⊢ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
11 10 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) → ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ∈ V )
12 1 5 7 11 fvmptd2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) → ( 𝐶 ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) )
13 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
14 13 sseq1d ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ↔ 𝑅 ⊆ 𝑠 ) )
15 14 anbi1d ⊢ ( 𝑅 ∈ 𝑉 → ( ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ↔ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) )
16 oveq2 ⊢ ( 𝑥 = 1 → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 1 ) )
17 16 sseq1d ⊢ ( 𝑥 = 1 → ( ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ) )
18 17 imbi2d ⊢ ( 𝑥 = 1 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ) ) )
19 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 𝑦 ) )
20 19 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) )
21 20 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) ) )
22 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) )
23 22 sseq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ 𝑠 ) )
24 23 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ 𝑠 ) ) )
25 oveq2 ⊢ ( 𝑥 = 𝑛 → ( 𝑅 ↑𝑟 𝑥 ) = ( 𝑅 ↑𝑟 𝑛 ) )
26 25 sseq1d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ↔ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
27 26 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑥 ) ⊆ 𝑠 ) ↔ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) ) )
28 simprl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 )
29 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → 𝑦 ∈ ℕ )
30 1nn ⊢ 1 ∈ ℕ
31 30 a1i ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → 1 ∈ ℕ )
32 simp2l ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → 𝑅 ∈ 𝑉 )
33 relexpaddnn ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 1 ) ) = ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) )
34 29 31 32 33 syl3anc ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( ( 𝑅 ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 1 ) ) = ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) )
35 simp2rr ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 )
36 simp3 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 )
37 simp2rl ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 )
38 35 36 37 trrelssd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( ( 𝑅 ↑𝑟 𝑦 ) ∘ ( 𝑅 ↑𝑟 1 ) ) ⊆ 𝑠 )
39 34 38 eqsstrrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ∧ ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ 𝑠 )
40 39 3exp ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 → ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ 𝑠 ) ) )
41 40 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑦 ) ⊆ 𝑠 ) → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 ( 𝑦 + 1 ) ) ⊆ 𝑠 ) ) )
42 18 21 24 27 28 41 nnind ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
43 42 com12 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ( 𝑛 ∈ ℕ → ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
44 43 ralrimiv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ∀ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
45 iunss ⊢ ( ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ↔ ∀ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
46 44 45 sylibr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) → ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 )
47 46 ex ⊢ ( 𝑅 ∈ 𝑉 → ( ( ( 𝑅 ↑𝑟 1 ) ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
48 15 47 sylbird ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
49 48 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) → ( ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
50 sseq1 ⊢ ( ( 𝐶 ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) → ( ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ↔ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) )
51 50 imbi2d ⊢ ( ( 𝐶 ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) → ( ( ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ) ↔ ( ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ⊆ 𝑠 ) ) )
52 49 51 syl5ibr ⊢ ( ( 𝐶 ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) → ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) → ( ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ) ) )
53 12 52 mpcom ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) → ( ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ) )
54 53 alrimiv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ ) → ∀ 𝑠 ( ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( 𝐶 ‘ 𝑅 ) ⊆ 𝑠 ) )