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 syl5ibr ( 𝑥 = ( 𝑦 ∪ ( 𝑋 𝑋 ) ) → ( ( 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 syl5ibr ( 𝑦 = 𝑥 → ( ( 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 unexg ( ( dom 𝑋 ∈ V ∧ ran 𝑋 ∈ V ) → ( dom 𝑋 ∪ ran 𝑋 ) ∈ V )
73 70 71 72 syl2anc ( 𝑋𝑉 → ( dom 𝑋 ∪ ran 𝑋 ) ∈ V )
74 73 resiexd ( 𝑋𝑉 → ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ∈ V )
75 unexg ( ( 𝑋𝑉 ∧ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ∈ V ) → ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∈ V )
76 74 75 mpdan ( 𝑋𝑉 → ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∈ V )
77 dmun dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) = ( dom 𝑋 ∪ dom ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) )
78 ssun1 dom 𝑋 ⊆ ( dom 𝑋 ∪ ran 𝑋 )
79 dmresi dom ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) = ( dom 𝑋 ∪ ran 𝑋 )
80 79 eqimssi dom ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
81 78 80 unssi ( dom 𝑋 ∪ dom ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
82 77 81 eqsstri dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
83 rnun ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) = ( ran 𝑋 ∪ ran ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) )
84 ssun2 ran 𝑋 ⊆ ( dom 𝑋 ∪ ran 𝑋 )
85 rnresi ran ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) = ( dom 𝑋 ∪ ran 𝑋 )
86 85 eqimssi ran ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
87 84 86 unssi ( ran 𝑋 ∪ ran ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
88 83 87 eqsstri ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 )
89 82 88 pm3.2i ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) ∧ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) )
90 unss ( ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) ∧ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) ) ↔ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) )
91 ssres2 ( ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ⊆ ( dom 𝑋 ∪ ran 𝑋 ) → ( I ↾ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ) ⊆ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) )
92 90 91 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 𝑋 ) ) )
93 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 𝑋 ) ) ) )
94 89 92 93 mp2b ( I ↾ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ) ⊆ ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) )
95 94 a1i ( 𝑋𝑉 → ( I ↾ ( dom ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ∪ ran ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) ) ) ⊆ ( 𝑋 ∪ ( I ↾ ( dom 𝑋 ∪ ran 𝑋 ) ) ) )
96 44 61 67 69 76 95 clcnvlem ( 𝑋𝑉 { 𝑥 ∣ ( 𝑋𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) } = { 𝑦 ∣ ( 𝑋𝑦 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) } )