Mathbox for Richard Penner < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cnvtrcl0 Structured version   Visualization version   GIF version

Theorem cnvtrcl0 37449
 Description: The converse of the transitive closure is equal to the closure of the converse. (Contributed by RP, 18-Oct-2020.)
Assertion
Ref Expression
cnvtrcl0 (𝑋𝑉 {𝑥 ∣ (𝑋𝑥 ∧ (𝑥𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑋𝑦 ∧ (𝑦𝑦) ⊆ 𝑦)})
Distinct variable groups:   𝑥,𝑦,𝑉   𝑥,𝑋,𝑦

Proof of Theorem cnvtrcl0
StepHypRef Expression
1 cnvco 5273 . . . . . 6 (𝑦𝑦) = (𝑦𝑦)
2 cnvss 5259 . . . . . 6 ((𝑦𝑦) ⊆ 𝑦(𝑦𝑦) ⊆ 𝑦)
31, 2syl5eqssr 3634 . . . . 5 ((𝑦𝑦) ⊆ 𝑦 → (𝑦𝑦) ⊆ 𝑦)
4 coundir 5601 . . . . . . 7 ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) = ((𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ∪ ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))))
5 coundi 5600 . . . . . . . . 9 (𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) = ((𝑦𝑦) ∪ (𝑦 ∘ (𝑋𝑋)))
6 ssid 3608 . . . . . . . . . 10 (𝑦𝑦) ⊆ (𝑦𝑦)
7 cononrel2 37417 . . . . . . . . . . 11 (𝑦 ∘ (𝑋𝑋)) = ∅
8 0ss 3949 . . . . . . . . . . 11 ∅ ⊆ (𝑦𝑦)
97, 8eqsstri 3619 . . . . . . . . . 10 (𝑦 ∘ (𝑋𝑋)) ⊆ (𝑦𝑦)
106, 9unssi 3771 . . . . . . . . 9 ((𝑦𝑦) ∪ (𝑦 ∘ (𝑋𝑋))) ⊆ (𝑦𝑦)
115, 10eqsstri 3619 . . . . . . . 8 (𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
12 cononrel1 37416 . . . . . . . . 9 ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))) = ∅
1312, 8eqsstri 3619 . . . . . . . 8 ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
1411, 13unssi 3771 . . . . . . 7 ((𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ∪ ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋)))) ⊆ (𝑦𝑦)
154, 14eqsstri 3619 . . . . . 6 ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
16 id 22 . . . . . 6 ((𝑦𝑦) ⊆ 𝑦 → (𝑦𝑦) ⊆ 𝑦)
1715, 16syl5ss 3598 . . . . 5 ((𝑦𝑦) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ 𝑦)
18 ssun3 3761 . . . . 5 (((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋)))
193, 17, 183syl 18 . . . 4 ((𝑦𝑦) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋)))
20 id 22 . . . . . 6 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → 𝑥 = (𝑦 ∪ (𝑋𝑋)))
2120, 20coeq12d 5251 . . . . 5 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → (𝑥𝑥) = ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))))
2221, 20sseq12d 3618 . . . 4 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → ((𝑥𝑥) ⊆ 𝑥 ↔ ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋))))
2319, 22syl5ibr 236 . . 3 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → ((𝑦𝑦) ⊆ 𝑦 → (𝑥𝑥) ⊆ 𝑥))
2423adantl 482 . 2 ((𝑋𝑉𝑥 = (𝑦 ∪ (𝑋𝑋))) → ((𝑦𝑦) ⊆ 𝑦 → (𝑥𝑥) ⊆ 𝑥))
25 cnvco 5273 . . . . 5 (𝑥𝑥) = (𝑥𝑥)
26 cnvss 5259 . . . . 5 ((𝑥𝑥) ⊆ 𝑥(𝑥𝑥) ⊆ 𝑥)
2725, 26syl5eqssr 3634 . . . 4 ((𝑥𝑥) ⊆ 𝑥 → (𝑥𝑥) ⊆ 𝑥)
28 id 22 . . . . . 6 (𝑦 = 𝑥𝑦 = 𝑥)
2928, 28coeq12d 5251 . . . . 5 (𝑦 = 𝑥 → (𝑦𝑦) = (𝑥𝑥))
3029, 28sseq12d 3618 . . . 4 (𝑦 = 𝑥 → ((𝑦𝑦) ⊆ 𝑦 ↔ (𝑥𝑥) ⊆ 𝑥))
3127, 30syl5ibr 236 . . 3 (𝑦 = 𝑥 → ((𝑥𝑥) ⊆ 𝑥 → (𝑦𝑦) ⊆ 𝑦))
3231adantl 482 . 2 ((𝑋𝑉𝑦 = 𝑥) → ((𝑥𝑥) ⊆ 𝑥 → (𝑦𝑦) ⊆ 𝑦))
33 id 22 . . . 4 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → 𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
3433, 33coeq12d 5251 . . 3 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → (𝑥𝑥) = ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
3534, 33sseq12d 3618 . 2 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → ((𝑥𝑥) ⊆ 𝑥 ↔ ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
36 ssun1 3759 . . 3 𝑋 ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
3736a1i 11 . 2 (𝑋𝑉𝑋 ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
38 trclexlem 13675 . 2 (𝑋𝑉 → (𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∈ V)
39 coundir 5601 . . . . 5 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = ((𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ∪ ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
40 coundi 5600 . . . . . . 7 (𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = ((𝑋𝑋) ∪ (𝑋 ∘ (dom 𝑋 × ran 𝑋)))
41 cossxp 5622 . . . . . . . 8 (𝑋𝑋) ⊆ (dom 𝑋 × ran 𝑋)
42 cossxp 5622 . . . . . . . . 9 (𝑋 ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom (dom 𝑋 × ran 𝑋) × ran 𝑋)
43 dmxpss 5529 . . . . . . . . . 10 dom (dom 𝑋 × ran 𝑋) ⊆ dom 𝑋
44 xpss1 5194 . . . . . . . . . 10 (dom (dom 𝑋 × ran 𝑋) ⊆ dom 𝑋 → (dom (dom 𝑋 × ran 𝑋) × ran 𝑋) ⊆ (dom 𝑋 × ran 𝑋))
4543, 44ax-mp 5 . . . . . . . . 9 (dom (dom 𝑋 × ran 𝑋) × ran 𝑋) ⊆ (dom 𝑋 × ran 𝑋)
4642, 45sstri 3596 . . . . . . . 8 (𝑋 ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
4741, 46unssi 3771 . . . . . . 7 ((𝑋𝑋) ∪ (𝑋 ∘ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
4840, 47eqsstri 3619 . . . . . 6 (𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
49 coundi 5600 . . . . . . 7 ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = (((dom 𝑋 × ran 𝑋) ∘ 𝑋) ∪ ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋)))
50 cossxp 5622 . . . . . . . . 9 ((dom 𝑋 × ran 𝑋) ∘ 𝑋) ⊆ (dom 𝑋 × ran (dom 𝑋 × ran 𝑋))
51 rnxpss 5530 . . . . . . . . . 10 ran (dom 𝑋 × ran 𝑋) ⊆ ran 𝑋
52 xpss2 5195 . . . . . . . . . 10 (ran (dom 𝑋 × ran 𝑋) ⊆ ran 𝑋 → (dom 𝑋 × ran (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋))
5351, 52ax-mp 5 . . . . . . . . 9 (dom 𝑋 × ran (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
5450, 53sstri 3596 . . . . . . . 8 ((dom 𝑋 × ran 𝑋) ∘ 𝑋) ⊆ (dom 𝑋 × ran 𝑋)
55 xptrrel 13661 . . . . . . . 8 ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
5654, 55unssi 3771 . . . . . . 7 (((dom 𝑋 × ran 𝑋) ∘ 𝑋) ∪ ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
5749, 56eqsstri 3619 . . . . . 6 ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
5848, 57unssi 3771 . . . . 5 ((𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ∪ ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))) ⊆ (dom 𝑋 × ran 𝑋)
5939, 58eqsstri 3619 . . . 4 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
60 ssun2 3760 . . . 4 (dom 𝑋 × ran 𝑋) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
6159, 60sstri 3596 . . 3 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
6261a1i 11 . 2 (𝑋𝑉 → ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
6324, 32, 35, 37, 38, 62clcnvlem 37446 1 (𝑋𝑉 {𝑥 ∣ (𝑋𝑥 ∧ (𝑥𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑋𝑦 ∧ (𝑦𝑦) ⊆ 𝑦)})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  {cab 2607   ∖ cdif 3556   ∪ cun 3557   ⊆ wss 3559  ∅c0 3896  ∩ cint 4445   × cxp 5077  ◡ccnv 5078  dom cdm 5079  ran crn 5080   ∘ ccom 5083 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-int 4446  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-iota 5815  df-fun 5854  df-fv 5860  df-1st 7120  df-2nd 7121 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator