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 syl5bi ( 𝑟 ∈ 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 ( 𝑟𝑟 𝑛 ) )