Metamath Proof Explorer

Theorem cnvtrcl0

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

Ref Expression
Assertion cnvtrcl0 ( 𝑋 ∈ 𝑉 → ◡ ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } = ∩ { 𝑦 ∣ ( ◡ 𝑋 ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) } )

Proof

Step Hyp Ref Expression
1 cnvco ⊢ ◡ ( 𝑦 ∘ 𝑦 ) = ( ◡ 𝑦 ∘ ◡ 𝑦 )
2 cnvss ⊢ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 → ◡ ( 𝑦 ∘ 𝑦 ) ⊆ ◡ 𝑦 )
3 1 2 eqsstrrid ⊢ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 → ( ◡ 𝑦 ∘ ◡ 𝑦 ) ⊆ ◡ 𝑦 )
4 coundir ⊢ ( ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) = ( ( ◡ 𝑦 ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ∪ ( ( 𝑋 ∖ ◡ ◡ 𝑋 ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) )
5 coundi ⊢ ( ◡ 𝑦 ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) = ( ( ◡ 𝑦 ∘ ◡ 𝑦 ) ∪ ( ◡ 𝑦 ∘ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
6 ssid ⊢ ( ◡ 𝑦 ∘ ◡ 𝑦 ) ⊆ ( ◡ 𝑦 ∘ ◡ 𝑦 )
7 cononrel2 ⊢ ( ◡ 𝑦 ∘ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) = ∅
8 0ss ⊢ ∅ ⊆ ( ◡ 𝑦 ∘ ◡ 𝑦 )
9 7 8 eqsstri ⊢ ( ◡ 𝑦 ∘ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ⊆ ( ◡ 𝑦 ∘ ◡ 𝑦 )
10 6 9 unssi ⊢ ( ( ◡ 𝑦 ∘ ◡ 𝑦 ) ∪ ( ◡ 𝑦 ∘ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ⊆ ( ◡ 𝑦 ∘ ◡ 𝑦 )
11 5 10 eqsstri ⊢ ( ◡ 𝑦 ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ⊆ ( ◡ 𝑦 ∘ ◡ 𝑦 )
12 cononrel1 ⊢ ( ( 𝑋 ∖ ◡ ◡ 𝑋 ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) = ∅
13 12 8 eqsstri ⊢ ( ( 𝑋 ∖ ◡ ◡ 𝑋 ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ⊆ ( ◡ 𝑦 ∘ ◡ 𝑦 )
14 11 13 unssi ⊢ ( ( ◡ 𝑦 ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ∪ ( ( 𝑋 ∖ ◡ ◡ 𝑋 ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ) ⊆ ( ◡ 𝑦 ∘ ◡ 𝑦 )
15 4 14 eqsstri ⊢ ( ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ⊆ ( ◡ 𝑦 ∘ ◡ 𝑦 )
16 id ⊢ ( ( ◡ 𝑦 ∘ ◡ 𝑦 ) ⊆ ◡ 𝑦 → ( ◡ 𝑦 ∘ ◡ 𝑦 ) ⊆ ◡ 𝑦 )
17 15 16 sstrid ⊢ ( ( ◡ 𝑦 ∘ ◡ 𝑦 ) ⊆ ◡ 𝑦 → ( ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ⊆ ◡ 𝑦 )
18 ssun3 ⊢ ( ( ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ⊆ ◡ 𝑦 → ( ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
19 3 17 18 3syl ⊢ ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 → ( ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
20 id ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) )
21 20 20 coeq12d ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ( 𝑥 ∘ 𝑥 ) = ( ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) )
22 21 20 sseq12d ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ↔ ( ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ∘ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) ⊆ ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) )
23 19 22 imbitrrid ⊢ ( 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) → ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 → ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) )
24 23 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 = ( ◡ 𝑦 ∪ ( 𝑋 ∖ ◡ ◡ 𝑋 ) ) ) → ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 → ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) )
25 cnvco ⊢ ◡ ( 𝑥 ∘ 𝑥 ) = ( ◡ 𝑥 ∘ ◡ 𝑥 )
26 cnvss ⊢ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 → ◡ ( 𝑥 ∘ 𝑥 ) ⊆ ◡ 𝑥 )
27 25 26 eqsstrrid ⊢ ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 → ( ◡ 𝑥 ∘ ◡ 𝑥 ) ⊆ ◡ 𝑥 )
28 id ⊢ ( 𝑦 = ◡ 𝑥 → 𝑦 = ◡ 𝑥 )
29 28 28 coeq12d ⊢ ( 𝑦 = ◡ 𝑥 → ( 𝑦 ∘ 𝑦 ) = ( ◡ 𝑥 ∘ ◡ 𝑥 ) )
30 29 28 sseq12d ⊢ ( 𝑦 = ◡ 𝑥 → ( ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ↔ ( ◡ 𝑥 ∘ ◡ 𝑥 ) ⊆ ◡ 𝑥 ) )
31 27 30 imbitrrid ⊢ ( 𝑦 = ◡ 𝑥 → ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 → ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) )
32 31 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑦 = ◡ 𝑥 ) → ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 → ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) )
33 id ⊢ ( 𝑥 = ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) → 𝑥 = ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) )
34 33 33 coeq12d ⊢ ( 𝑥 = ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) → ( 𝑥 ∘ 𝑥 ) = ( ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) )
35 34 33 sseq12d ⊢ ( 𝑥 = ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) → ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ↔ ( ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) ⊆ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) )
36 ssun1 ⊢ 𝑋 ⊆ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) )
37 36 a1i ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ⊆ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) )
38 trclexlem ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ∈ V )
39 coundir ⊢ ( ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) = ( ( 𝑋 ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) ∪ ( ( dom 𝑋 × ran 𝑋 ) ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) )
40 coundi ⊢ ( 𝑋 ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) = ( ( 𝑋 ∘ 𝑋 ) ∪ ( 𝑋 ∘ ( dom 𝑋 × ran 𝑋 ) ) )
41 cossxp ⊢ ( 𝑋 ∘ 𝑋 ) ⊆ ( dom 𝑋 × ran 𝑋 )
42 cossxp ⊢ ( 𝑋 ∘ ( dom 𝑋 × ran 𝑋 ) ) ⊆ ( dom ( dom 𝑋 × ran 𝑋 ) × ran 𝑋 )
43 dmxpss ⊢ dom ( dom 𝑋 × ran 𝑋 ) ⊆ dom 𝑋
44 xpss1 ⊢ ( dom ( dom 𝑋 × ran 𝑋 ) ⊆ dom 𝑋 → ( dom ( dom 𝑋 × ran 𝑋 ) × ran 𝑋 ) ⊆ ( dom 𝑋 × ran 𝑋 ) )
45 43 44 ax-mp ⊢ ( dom ( dom 𝑋 × ran 𝑋 ) × ran 𝑋 ) ⊆ ( dom 𝑋 × ran 𝑋 )
46 42 45 sstri ⊢ ( 𝑋 ∘ ( dom 𝑋 × ran 𝑋 ) ) ⊆ ( dom 𝑋 × ran 𝑋 )
47 41 46 unssi ⊢ ( ( 𝑋 ∘ 𝑋 ) ∪ ( 𝑋 ∘ ( dom 𝑋 × ran 𝑋 ) ) ) ⊆ ( dom 𝑋 × ran 𝑋 )
48 40 47 eqsstri ⊢ ( 𝑋 ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) ⊆ ( dom 𝑋 × ran 𝑋 )
49 coundi ⊢ ( ( dom 𝑋 × ran 𝑋 ) ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) = ( ( ( dom 𝑋 × ran 𝑋 ) ∘ 𝑋 ) ∪ ( ( dom 𝑋 × ran 𝑋 ) ∘ ( dom 𝑋 × ran 𝑋 ) ) )
50 cossxp ⊢ ( ( dom 𝑋 × ran 𝑋 ) ∘ 𝑋 ) ⊆ ( dom 𝑋 × ran ( dom 𝑋 × ran 𝑋 ) )
51 rnxpss ⊢ ran ( dom 𝑋 × ran 𝑋 ) ⊆ ran 𝑋
52 xpss2 ⊢ ( ran ( dom 𝑋 × ran 𝑋 ) ⊆ ran 𝑋 → ( dom 𝑋 × ran ( dom 𝑋 × ran 𝑋 ) ) ⊆ ( dom 𝑋 × ran 𝑋 ) )
53 51 52 ax-mp ⊢ ( dom 𝑋 × ran ( dom 𝑋 × ran 𝑋 ) ) ⊆ ( dom 𝑋 × ran 𝑋 )
54 50 53 sstri ⊢ ( ( dom 𝑋 × ran 𝑋 ) ∘ 𝑋 ) ⊆ ( dom 𝑋 × ran 𝑋 )
55 xptrrel ⊢ ( ( dom 𝑋 × ran 𝑋 ) ∘ ( dom 𝑋 × ran 𝑋 ) ) ⊆ ( dom 𝑋 × ran 𝑋 )
56 54 55 unssi ⊢ ( ( ( dom 𝑋 × ran 𝑋 ) ∘ 𝑋 ) ∪ ( ( dom 𝑋 × ran 𝑋 ) ∘ ( dom 𝑋 × ran 𝑋 ) ) ) ⊆ ( dom 𝑋 × ran 𝑋 )
57 49 56 eqsstri ⊢ ( ( dom 𝑋 × ran 𝑋 ) ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) ⊆ ( dom 𝑋 × ran 𝑋 )
58 48 57 unssi ⊢ ( ( 𝑋 ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) ∪ ( ( dom 𝑋 × ran 𝑋 ) ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) ) ⊆ ( dom 𝑋 × ran 𝑋 )
59 39 58 eqsstri ⊢ ( ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) ⊆ ( dom 𝑋 × ran 𝑋 )
60 ssun2 ⊢ ( dom 𝑋 × ran 𝑋 ) ⊆ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) )
61 59 60 sstri ⊢ ( ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) ⊆ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) )
62 61 a1i ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ∘ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) ) ⊆ ( 𝑋 ∪ ( dom 𝑋 × ran 𝑋 ) ) )
63 24 32 35 37 38 62 clcnvlem ⊢ ( 𝑋 ∈ 𝑉 → ◡ ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } = ∩ { 𝑦 ∣ ( ◡ 𝑋 ⊆ 𝑦 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) } )