# Metamath Proof Explorer

## Theorem dfrtrcl5

Description: Definition of reflexive-transitive closure as a standard closure. (Contributed by RP, 1-Nov-2020)

Ref Expression
Assertion dfrtrcl5 t* = ( 𝑥 ∈ V ↦ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦𝑦 ) ⊆ 𝑦 ) ) } )

### Proof

Step Hyp Ref Expression
1 df-rtrcl t* = ( 𝑥 ∈ V ↦ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } )
2 ancom ( ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦𝑦 ) ⊆ 𝑦 ) ↔ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) )
3 2 anbi2i ( ( 𝑥𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦𝑦 ) ⊆ 𝑦 ) ) ↔ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) )
4 3 abbii { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦𝑦 ) ⊆ 𝑦 ) ) } = { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) }
5 4 inteqi { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦𝑦 ) ⊆ 𝑦 ) ) } = { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) }
6 5 mpteq2i ( 𝑥 ∈ V ↦ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦𝑦 ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ V ↦ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } )
7 vex 𝑥 ∈ V
8 7 rtrclexi { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∈ V
9 8 a1i ( 𝑥 ∈ V → { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∈ V )
10 dmexg ( 𝑥 ∈ V → dom 𝑥 ∈ V )
11 rnexg ( 𝑥 ∈ V → ran 𝑥 ∈ V )
12 unexg ( ( dom 𝑥 ∈ V ∧ ran 𝑥 ∈ V ) → ( dom 𝑥 ∪ ran 𝑥 ) ∈ V )
13 10 11 12 syl2anc ( 𝑥 ∈ V → ( dom 𝑥 ∪ ran 𝑥 ) ∈ V )
14 resiexg ( ( dom 𝑥 ∪ ran 𝑥 ) ∈ V → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∈ V )
15 7 13 14 mp2b ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∈ V
16 7 15 unex ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ∈ V
17 16 trclexi { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∈ V
18 17 a1i ( 𝑥 ∈ V → { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∈ V )
19 simpr ( ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) → ( 𝑧𝑧 ) ⊆ 𝑧 )
20 19 cotrintab ( { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∘ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) ⊆ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) }
21 20 a1i ( 𝑥 ∈ V → ( { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∘ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) ⊆ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } )
22 7 dmex dom 𝑥 ∈ V
23 7 rnex ran 𝑥 ∈ V
24 12 resiexd ( ( dom 𝑥 ∈ V ∧ ran 𝑥 ∈ V ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∈ V )
25 22 23 24 mp2an ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∈ V
26 7 25 unex ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ∈ V
27 dmtrcl ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ∈ V → dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } = dom ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) )
28 26 27 ax-mp dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } = dom ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) )
29 dmun dom ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( dom 𝑥 ∪ dom ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) )
30 dmresi dom ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 )
31 30 uneq2i ( dom 𝑥 ∪ dom ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( dom 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) )
32 ssun1 dom 𝑥 ⊆ ( dom 𝑥 ∪ ran 𝑥 )
33 ssequn1 ( dom 𝑥 ⊆ ( dom 𝑥 ∪ ran 𝑥 ) ↔ ( dom 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 ) )
34 32 33 mpbi ( dom 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 )
35 29 31 34 3eqtri dom ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( dom 𝑥 ∪ ran 𝑥 )
36 28 35 eqtri dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } = ( dom 𝑥 ∪ ran 𝑥 )
37 rntrcl ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ∈ V → ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } = ran ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) )
38 26 37 ax-mp ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } = ran ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) )
39 rnun ran ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( ran 𝑥 ∪ ran ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) )
40 rnresi ran ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 )
41 40 uneq2i ( ran 𝑥 ∪ ran ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( ran 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) )
42 ssun2 ran 𝑥 ⊆ ( dom 𝑥 ∪ ran 𝑥 )
43 ssequn1 ( ran 𝑥 ⊆ ( dom 𝑥 ∪ ran 𝑥 ) ↔ ( ran 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 ) )
44 42 43 mpbi ( ran 𝑥 ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 )
45 39 41 44 3eqtri ran ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) = ( dom 𝑥 ∪ ran 𝑥 )
46 38 45 eqtri ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } = ( dom 𝑥 ∪ ran 𝑥 )
47 36 46 uneq12i ( dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∪ ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) = ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ ( dom 𝑥 ∪ ran 𝑥 ) )
48 unidm ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 )
49 47 48 eqtri ( dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∪ ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) = ( dom 𝑥 ∪ ran 𝑥 )
50 49 reseq2i ( I ↾ ( dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∪ ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) ) = ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) )
51 ssun2 ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) )
52 ssmin ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) }
53 51 52 sstri ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) }
54 50 53 eqsstri ( I ↾ ( dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∪ ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) ) ⊆ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) }
55 54 a1i ( 𝑥 ∈ V → ( I ↾ ( dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∪ ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) ) ⊆ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } )
56 simprl ( ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → ( 𝑦𝑦 ) ⊆ 𝑦 )
57 56 cotrintab ( { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∘ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) ⊆ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) }
58 57 a1i ( 𝑥 ∈ V → ( { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∘ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) ⊆ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } )
59 id ( 𝑦 = { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } → 𝑦 = { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } )
60 59 59 coeq12d ( 𝑦 = { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } → ( 𝑦𝑦 ) = ( { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∘ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) )
61 60 59 sseq12d ( 𝑦 = { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } → ( ( 𝑦𝑦 ) ⊆ 𝑦 ↔ ( { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∘ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) ⊆ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) )
62 dmeq ( 𝑦 = { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } → dom 𝑦 = dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } )
63 rneq ( 𝑦 = { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } → ran 𝑦 = ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } )
64 62 63 uneq12d ( 𝑦 = { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } → ( dom 𝑦 ∪ ran 𝑦 ) = ( dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∪ ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) )
65 64 reseq2d ( 𝑦 = { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } → ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) = ( I ↾ ( dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∪ ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) ) )
66 65 59 sseq12d ( 𝑦 = { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } → ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ↔ ( I ↾ ( dom { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ∪ ran { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) ) ⊆ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) )
67 id ( 𝑧 = { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } → 𝑧 = { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } )
68 67 67 coeq12d ( 𝑧 = { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } → ( 𝑧𝑧 ) = ( { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∘ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) )
69 68 67 sseq12d ( 𝑧 = { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } → ( ( 𝑧𝑧 ) ⊆ 𝑧 ↔ ( { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∘ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) ⊆ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) )
70 9 18 21 55 58 61 66 69 mptrcllem ( 𝑥 ∈ V ↦ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( 𝑦𝑦 ) ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ V ↦ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } )
71 df-3an ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) ↔ ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ) ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) )
72 ancom ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ) ↔ ( 𝑥𝑧 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ) )
73 unss ( ( 𝑥𝑧 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 ) ↔ ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 )
74 72 73 bitri ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ) ↔ ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 )
75 74 anbi1i ( ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ) ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) ↔ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) )
76 71 75 bitr2i ( ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) )
77 76 abbii { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } = { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) }
78 77 inteqi { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } = { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) }
79 78 mpteq2i ( 𝑥 ∈ V ↦ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } ) = ( 𝑥 ∈ V ↦ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } )
80 6 70 79 3eqtri ( 𝑥 ∈ V ↦ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦𝑦 ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ V ↦ { 𝑧 ∣ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧𝑥𝑧 ∧ ( 𝑧𝑧 ) ⊆ 𝑧 ) } )
81 1 80 eqtr4i t* = ( 𝑥 ∈ V ↦ { 𝑦 ∣ ( 𝑥𝑦 ∧ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ∧ ( 𝑦𝑦 ) ⊆ 𝑦 ) ) } )