Metamath Proof Explorer

Theorem dftrcl3

Description: Transitive closure of a relation, expressed as indexed union of powers of relations. (Contributed by RP, 5-Jun-2020)

Ref Expression
Assertion dftrcl3 t+ = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )

Proof

Step Hyp Ref Expression
1 df-trcl ⊢ t+ = ( 𝑟 ∈ V ↦ ∩ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
2 relexp1g ⊢ ( 𝑟 ∈ V → ( 𝑟 ↑𝑟 1 ) = 𝑟 )
3 nnex ⊢ ℕ ∈ V
4 1nn ⊢ 1 ∈ ℕ
5 oveq1 ⊢ ( 𝑎 = 𝑡 → ( 𝑎 ↑𝑟 𝑛 ) = ( 𝑡 ↑𝑟 𝑛 ) )
6 5 iuneq2d ⊢ ( 𝑎 = 𝑡 → ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ( 𝑡 ↑𝑟 𝑛 ) )
7 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑡 ↑𝑟 𝑛 ) = ( 𝑡 ↑𝑟 𝑘 ) )
8 7 cbviunv ⊢ ∪ 𝑛 ∈ ℕ ( 𝑡 ↑𝑟 𝑛 ) = ∪ 𝑘 ∈ ℕ ( 𝑡 ↑𝑟 𝑘 )
9 6 8 eqtrdi ⊢ ( 𝑎 = 𝑡 → ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) = ∪ 𝑘 ∈ ℕ ( 𝑡 ↑𝑟 𝑘 ) )
10 9 cbvmptv ⊢ ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) = ( 𝑡 ∈ V ↦ ∪ 𝑘 ∈ ℕ ( 𝑡 ↑𝑟 𝑘 ) )
11 10 ov2ssiunov2 ⊢ ( ( 𝑟 ∈ V ∧ ℕ ∈ V ∧ 1 ∈ ℕ ) → ( 𝑟 ↑𝑟 1 ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
12 3 4 11 mp3an23 ⊢ ( 𝑟 ∈ V → ( 𝑟 ↑𝑟 1 ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
13 2 12 eqsstrrd ⊢ ( 𝑟 ∈ V → 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
14 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
15 1nn0 ⊢ 1 ∈ ℕ0
16 10 iunrelexpuztr ⊢ ( ( 𝑟 ∈ V ∧ ℕ = ( ℤ≥ ‘ 1 ) ∧ 1 ∈ ℕ0 ) → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
17 14 15 16 mp3an23 ⊢ ( 𝑟 ∈ V → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
18 fvex ⊢ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ V
19 trcleq2lem ⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) )
20 19 a1i ⊢ ( 𝑟 ∈ V → ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) )
21 20 alrimiv ⊢ ( 𝑟 ∈ V → ∀ 𝑧 ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) )
22 elabgt ⊢ ( ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ V ∧ ∀ 𝑧 ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) ) → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) )
23 18 21 22 sylancr ⊢ ( 𝑟 ∈ V → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) )
24 13 17 23 mpbir2and ⊢ ( 𝑟 ∈ V → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
25 intss1 ⊢ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ∩ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
26 24 25 syl ⊢ ( 𝑟 ∈ V → ∩ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
27 vex ⊢ 𝑠 ∈ V
28 trcleq2lem ⊢ ( 𝑧 = 𝑠 → ( ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) )
29 27 28 elab ⊢ ( 𝑠 ∈ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) )
30 eqid ⊢ ℕ = ℕ
31 10 iunrelexpmin1 ⊢ ( ( 𝑟 ∈ V ∧ ℕ = ℕ ) → ∀ 𝑠 ( ( 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) )
32 30 31 mpan2 ⊢ ( 𝑟 ∈ V → ∀ 𝑠 ( ( 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) )
33 32 19.21bi ⊢ ( 𝑟 ∈ V → ( ( 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) )
34 29 33 syl5bi ⊢ ( 𝑟 ∈ V → ( 𝑠 ∈ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) )
35 34 ralrimiv ⊢ ( 𝑟 ∈ V → ∀ 𝑠 ∈ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 )
36 ssint ⊢ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ ∩ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ∀ 𝑠 ∈ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 )
37 35 36 sylibr ⊢ ( 𝑟 ∈ V → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ ∩ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
38 26 37 eqssd ⊢ ( 𝑟 ∈ V → ∩ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
39 oveq1 ⊢ ( 𝑎 = 𝑟 → ( 𝑎 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 𝑛 ) )
40 39 iuneq2d ⊢ ( 𝑎 = 𝑟 → ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
41 eqid ⊢ ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) = ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) )
42 ovex ⊢ ( 𝑟 ↑𝑟 𝑛 ) ∈ V
43 3 42 iunex ⊢ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) ∈ V
44 40 41 43 fvmpt ⊢ ( 𝑟 ∈ V → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) = ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
45 38 44 eqtrd ⊢ ( 𝑟 ∈ V → ∩ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
46 45 mpteq2ia ⊢ ( 𝑟 ∈ V ↦ ∩ { 𝑧 ∣ ( 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
47 1 46 eqtri ⊢ t+ = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )