Metamath Proof Explorer

Theorem cnvrcl0

Description: The converse of the reflexive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020)

Ref Expression
Assertion cnvrcl0 ( 𝑋 ∈ 𝑉 → ◡ ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) } = ∩ { 𝑦 ∣ ( ◡ 𝑋 ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) } )

Proof

Step Hyp Ref Expression
1 cnvresid ⊢ ◡ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) = ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) )
2 cnvnonrel ⊢ ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) = ∅
3 cnv0 ⊢ ◡ ∅ = ∅
4 2 3 eqtr4i ⊢ ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) = ◡ ∅
5 4 dmeqi ⊢ dom ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) = dom ◡ ∅
6 df-rn ⊢ ran ( 𝑋 ∖ ◡ ◡ 𝑋 ) = dom ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 )
7 df-rn ⊢ ran ∅ = dom ◡ ∅
8 5 6 7 3eqtr4i ⊢ ran ( 𝑋 ∖ ◡ ◡ 𝑋 ) = ran ∅
9 0ss ⊢ ∅ ⊆ ◡ 𝑦
10 9 rnssi ⊢ ran ∅ ⊆ ran ◡ 𝑦
11 8 10 eqsstri ⊢ ran ( 𝑋 ∖ ◡ ◡ 𝑋 ) ⊆ ran ◡ 𝑦
12 ssequn2 ⊢ ( ran ( 𝑋 ∖ ◡ ◡ 𝑋 ) ⊆ ran ◡ 𝑦 ↔ ( ran ◡ 𝑦 ∪ ran ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = ran ◡ 𝑦 )
13 11 12 mpbi ⊢ ( ran ◡ 𝑦 ∪ ran ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = ran ◡ 𝑦
14 rnun ⊢ ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = ( ran ◡ 𝑦 ∪ ran ( 𝑋 ∖ ◡ ◡ 𝑋 ) )
15 dfdm4 ⊢ dom 𝑦 = ran ◡ 𝑦
16 13 14 15 3eqtr4ri ⊢ dom 𝑦 = ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) )
17 4 rneqi ⊢ ran ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 ) = ran ◡ ∅
18 dfdm4 ⊢ dom ( 𝑋 ∖ ◡ ◡ 𝑋 ) = ran ◡ ( 𝑋 ∖ ◡ ◡ 𝑋 )
19 dfdm4 ⊢ dom ∅ = ran ◡ ∅
20 17 18 19 3eqtr4i ⊢ dom ( 𝑋 ∖ ◡ ◡ 𝑋 ) = dom ∅
21 dmss ⊢ ( ∅ ⊆ ◡ 𝑦 → dom ∅ ⊆ dom ◡ 𝑦 )
22 9 21 ax-mp ⊢ dom ∅ ⊆ dom ◡ 𝑦
23 20 22 eqsstri ⊢ dom ( 𝑋 ∖ ◡ ◡ 𝑋 ) ⊆ dom ◡ 𝑦
24 ssequn2 ⊢ ( dom ( 𝑋 ∖ ◡ ◡ 𝑋 ) ⊆ dom ◡ 𝑦 ↔ ( dom ◡ 𝑦 ∪ dom ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = dom ◡ 𝑦 )
25 23 24 mpbi ⊢ ( dom ◡ 𝑦 ∪ dom ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = dom ◡ 𝑦
26 dmun ⊢ dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = ( dom ◡ 𝑦 ∪ dom ( 𝑋 ∖ ◡ ◡ 𝑋 ) )
27 df-rn ⊢ ran 𝑦 = dom ◡ 𝑦
28 25 26 27 3eqtr4ri ⊢ ran 𝑦 = dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) )
29 16 28 uneq12i ⊢ ( dom 𝑦 ∪ ran 𝑦 ) = ( ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∪ dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
30 29 equncomi ⊢ ( dom 𝑦 ∪ ran 𝑦 ) = ( dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∪ ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
31 30 reseq2i ⊢ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) = ( I ↾ ( dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∪ ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) )
32 1 31 eqtr2i ⊢ ( I ↾ ( dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∪ ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ) = ◡ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) )
33 cnvss ⊢ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 → ◡ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ ◡ 𝑦 )
34 32 33 eqsstrid ⊢ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 → ( I ↾ ( dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∪ ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ) ⊆ ◡ 𝑦 )
35 ssun1 ⊢ ◡ 𝑦 ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) )
36 34 35 sstrdi ⊢ ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 → ( I ↾ ( dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∪ ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ) ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
37 dmeq ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → dom 𝑥 = dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
38 rneq ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ran 𝑥 = ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
39 37 38 uneq12d ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ( dom 𝑥 ∪ ran 𝑥 ) = ( dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∪ ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) )
40 39 reseq2d ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( I ↾ ( dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∪ ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ) )
41 id ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
42 40 41 sseq12d ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ↔ ( I ↾ ( dom ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∪ ran ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ) ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) )
43 36 42 imbitrrid ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) )
44 43 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) → ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) )
45 cnvresid ⊢ ◡ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) )
46 dfdm4 ⊢ dom 𝑥 = ran ◡ 𝑥
47 df-rn ⊢ ran 𝑥 = dom ◡ 𝑥
48 46 47 uneq12i ⊢ ( dom 𝑥 ∪ ran 𝑥 ) = ( ran ◡ 𝑥 ∪ dom ◡ 𝑥 )
49 48 equncomi ⊢ ( dom 𝑥 ∪ ran 𝑥 ) = ( dom ◡ 𝑥 ∪ ran ◡ 𝑥 )
50 49 reseq2i ⊢ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( I ↾ ( dom ◡ 𝑥 ∪ ran ◡ 𝑥 ) )
51 45 50 eqtr2i ⊢ ( I ↾ ( dom ◡ 𝑥 ∪ ran ◡ 𝑥 ) ) = ◡ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) )
52 cnvss ⊢ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 → ◡ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ◡ 𝑥 )
53 51 52 eqsstrid ⊢ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 → ( I ↾ ( dom ◡ 𝑥 ∪ ran ◡ 𝑥 ) ) ⊆ ◡ 𝑥 )
54 dmeq ⊢ ( 𝑦 = ◡ 𝑥 → dom 𝑦 = dom ◡ 𝑥 )
55 rneq ⊢ ( 𝑦 = ◡ 𝑥 → ran 𝑦 = ran ◡ 𝑥 )
56 54 55 uneq12d ⊢ ( 𝑦 = ◡ 𝑥 → ( dom 𝑦 ∪ ran 𝑦 ) = ( dom ◡ 𝑥 ∪ ran ◡ 𝑥 ) )
57 56 reseq2d ⊢ ( 𝑦 = ◡ 𝑥 → ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) = ( I ↾ ( dom ◡ 𝑥 ∪ ran ◡ 𝑥 ) ) )
58 id ⊢ ( 𝑦 = ◡ 𝑥 → 𝑦 = ◡ 𝑥 )
59 57 58 sseq12d ⊢ ( 𝑦 = ◡ 𝑥 → ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ↔ ( I ↾ ( dom ◡ 𝑥 ∪ ran ◡ 𝑥 ) ) ⊆ ◡ 𝑥 ) )
60 53 59 imbitrrid ⊢ ( 𝑦 = ◡ 𝑥 → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 → ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) )
61 60 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = ◡ 𝑥 ) → ( ( 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 id ⊢ ( 𝑥 = ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) → 𝑥 = ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) )
67 65 66 sseq12d ⊢ ( 𝑥 = ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ↔ ( I ↾ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ) ⊆ ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) )
68 ssun1 ⊢ 𝑋 ⊆ ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) )
69 68 a1i ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ⊆ ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) )
70 dmexg ⊢ ( 𝑋 ∈ 𝑉 → dom 𝑋 ∈ V )
71 rnexg ⊢ ( 𝑋 ∈ 𝑉 → ran 𝑋 ∈ V )
72 70 71 unexd ⊢ ( 𝑋 ∈ 𝑉 → ( dom 𝑋 ∪ ran 𝑋 ) ∈ V )
73 72 resiexd ⊢ ( 𝑋 ∈ 𝑉 → ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ∈ V )
74 unexg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ∈ V ) → ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∈ V )
75 73 74 mpdan ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∈ V )
76 dmun ⊢ dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) = ( dom 𝑋 ∪ dom ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) )
77 ssun1 ⊢ dom 𝑋 ⊆ ( dom 𝑋 ∪ ran 𝑋 )
78 resdmss ⊢ dom ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
79 77 78 unssi ⊢ ( dom 𝑋 ∪ dom ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
80 76 79 eqsstri ⊢ dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
81 rnun ⊢ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) = ( ran 𝑋 ∪ ran ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) )
82 ssun2 ⊢ ran 𝑋 ⊆ ( dom 𝑋 ∪ ran 𝑋 )
83 rnresi ⊢ ran ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) = ( dom 𝑋 ∪ ran 𝑋 )
84 83 eqimssi ⊢ ran ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
85 82 84 unssi ⊢ ( ran 𝑋 ∪ ran ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
86 81 85 eqsstri ⊢ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
87 80 86 pm3.2i ⊢ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) ∧ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) )
88 unss ⊢ ( ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) ∧ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) ) ↔ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) )
89 ssres2 ⊢ ( ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) → ( I ↾ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ) ⊆ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) )
90 88 89 sylbi ⊢ ( ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) ∧ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) ) → ( I ↾ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ) ⊆ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) )
91 ssun4 ⊢ ( ( I ↾ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ) ⊆ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) → ( I ↾ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ) ⊆ ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) )
92 87 90 91 mp2b ⊢ ( I ↾ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ) ⊆ ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) )
93 92 a1i ⊢ ( 𝑋 ∈ 𝑉 → ( I ↾ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ) ⊆ ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) )
94 44 61 67 69 75 93 clcnvlem ⊢ ( 𝑋 ∈ 𝑉 → ◡ ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) } = ∩ { 𝑦 ∣ ( ◡ 𝑋 ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) } )