Metamath Proof Explorer

Theorem dfrtrcl3

Description: Reflexive-transitive closure of a relation, expressed as indexed union of powers of relations. Generalized from dfrtrcl2 . (Contributed by RP, 5-Jun-2020)

Ref Expression
Assertion dfrtrcl3 t* = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )

Proof

Step Hyp Ref Expression
1 df-rtrcl ⊢ t* = ( 𝑟 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
2 relexp0g ⊢ ( 𝑟 ∈ V → ( 𝑟 ↑𝑟 0 ) = ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) )
3 nn0ex ⊢ ℕ0 ∈ V
4 0nn0 ⊢ 0 ∈ ℕ0
5 oveq1 ⊢ ( 𝑎 = 𝑡 → ( 𝑎 ↑𝑟 𝑛 ) = ( 𝑡 ↑𝑟 𝑛 ) )
6 5 iuneq2d ⊢ ( 𝑎 = 𝑡 → ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑡 ↑𝑟 𝑛 ) )
7 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑡 ↑𝑟 𝑛 ) = ( 𝑡 ↑𝑟 𝑘 ) )
8 7 cbviunv ⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑡 ↑𝑟 𝑛 ) = ∪ 𝑘 ∈ ℕ0 ( 𝑡 ↑𝑟 𝑘 )
9 6 8 eqtrdi ⊢ ( 𝑎 = 𝑡 → ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) = ∪ 𝑘 ∈ ℕ0 ( 𝑡 ↑𝑟 𝑘 ) )
10 9 cbvmptv ⊢ ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) = ( 𝑡 ∈ V ↦ ∪ 𝑘 ∈ ℕ0 ( 𝑡 ↑𝑟 𝑘 ) )
11 10 ov2ssiunov2 ⊢ ( ( 𝑟 ∈ V ∧ ℕ0 ∈ V ∧ 0 ∈ ℕ0 ) → ( 𝑟 ↑𝑟 0 ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
12 3 4 11 mp3an23 ⊢ ( 𝑟 ∈ V → ( 𝑟 ↑𝑟 0 ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
13 2 12 eqsstrrd ⊢ ( 𝑟 ∈ V → ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
14 relexp1g ⊢ ( 𝑟 ∈ V → ( 𝑟 ↑𝑟 1 ) = 𝑟 )
15 1nn0 ⊢ 1 ∈ ℕ0
16 10 ov2ssiunov2 ⊢ ( ( 𝑟 ∈ V ∧ ℕ0 ∈ V ∧ 1 ∈ ℕ0 ) → ( 𝑟 ↑𝑟 1 ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
17 3 15 16 mp3an23 ⊢ ( 𝑟 ∈ V → ( 𝑟 ↑𝑟 1 ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
18 14 17 eqsstrrd ⊢ ( 𝑟 ∈ V → 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
19 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
20 10 iunrelexpuztr ⊢ ( ( 𝑟 ∈ V ∧ ℕ0 = ( ℤ≥ ‘ 0 ) ∧ 0 ∈ ℕ0 ) → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
21 19 4 20 mp3an23 ⊢ ( 𝑟 ∈ V → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
22 fvex ⊢ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ V
23 sseq2 ⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ↔ ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) )
24 sseq2 ⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( 𝑟 ⊆ 𝑧 ↔ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) )
25 id ⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
26 25 25 coeq12d ⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( 𝑧 ∘ 𝑧 ) = ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) )
27 26 25 sseq12d ⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) )
28 23 24 27 3anbi123d ⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) )
29 28 a1i ⊢ ( 𝑟 ∈ V → ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) )
30 29 alrimiv ⊢ ( 𝑟 ∈ V → ∀ 𝑧 ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) )
31 elabgt ⊢ ( ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ V ∧ ∀ 𝑧 ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) ) → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) )
32 22 30 31 sylancr ⊢ ( 𝑟 ∈ V → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) )
33 13 18 21 32 mpbir3and ⊢ ( 𝑟 ∈ V → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
34 intss1 ⊢ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
35 33 34 syl ⊢ ( 𝑟 ∈ V → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
36 vex ⊢ 𝑠 ∈ V
37 sseq2 ⊢ ( 𝑧 = 𝑠 → ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ↔ ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ) )
38 sseq2 ⊢ ( 𝑧 = 𝑠 → ( 𝑟 ⊆ 𝑧 ↔ 𝑟 ⊆ 𝑠 ) )
39 id ⊢ ( 𝑧 = 𝑠 → 𝑧 = 𝑠 )
40 39 39 coeq12d ⊢ ( 𝑧 = 𝑠 → ( 𝑧 ∘ 𝑧 ) = ( 𝑠 ∘ 𝑠 ) )
41 40 39 sseq12d ⊢ ( 𝑧 = 𝑠 → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) )
42 37 38 41 3anbi123d ⊢ ( 𝑧 = 𝑠 → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ∧ 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) )
43 36 42 elab ⊢ ( 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ∧ 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) )
44 eqid ⊢ ℕ0 = ℕ0
45 10 iunrelexpmin2 ⊢ ( ( 𝑟 ∈ V ∧ ℕ0 = ℕ0 ) → ∀ 𝑠 ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ∧ 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) )
46 44 45 mpan2 ⊢ ( 𝑟 ∈ V → ∀ 𝑠 ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ∧ 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) )
47 46 19.21bi ⊢ ( 𝑟 ∈ V → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ∧ 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) )
48 43 47 biimtrid ⊢ ( 𝑟 ∈ V → ( 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) )
49 48 ralrimiv ⊢ ( 𝑟 ∈ V → ∀ 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 )
50 ssint ⊢ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ∀ 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 )
51 49 50 sylibr ⊢ ( 𝑟 ∈ V → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } )
52 35 51 eqssd ⊢ ( 𝑟 ∈ V → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) )
53 oveq1 ⊢ ( 𝑎 = 𝑟 → ( 𝑎 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 𝑛 ) )
54 53 iuneq2d ⊢ ( 𝑎 = 𝑟 → ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
55 eqid ⊢ ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) = ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) )
56 ovex ⊢ ( 𝑟 ↑𝑟 𝑛 ) ∈ V
57 3 56 iunex ⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ∈ V
58 54 55 57 fvmpt ⊢ ( 𝑟 ∈ V → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
59 52 58 eqtrd ⊢ ( 𝑟 ∈ V → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
60 59 mpteq2ia ⊢ ( 𝑟 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
61 1 60 eqtri ⊢ t* = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )