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

Theorem cnvtrcl0 38452
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 5444 . . . . . 6 (𝑦𝑦) = (𝑦𝑦)
2 cnvss 5431 . . . . . 6 ((𝑦𝑦) ⊆ 𝑦(𝑦𝑦) ⊆ 𝑦)
31, 2syl5eqssr 3799 . . . . 5 ((𝑦𝑦) ⊆ 𝑦 → (𝑦𝑦) ⊆ 𝑦)
4 coundir 5779 . . . . . . 7 ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) = ((𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ∪ ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))))
5 coundi 5778 . . . . . . . . 9 (𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) = ((𝑦𝑦) ∪ (𝑦 ∘ (𝑋𝑋)))
6 ssid 3773 . . . . . . . . . 10 (𝑦𝑦) ⊆ (𝑦𝑦)
7 cononrel2 38420 . . . . . . . . . . 11 (𝑦 ∘ (𝑋𝑋)) = ∅
8 0ss 4116 . . . . . . . . . . 11 ∅ ⊆ (𝑦𝑦)
97, 8eqsstri 3784 . . . . . . . . . 10 (𝑦 ∘ (𝑋𝑋)) ⊆ (𝑦𝑦)
106, 9unssi 3939 . . . . . . . . 9 ((𝑦𝑦) ∪ (𝑦 ∘ (𝑋𝑋))) ⊆ (𝑦𝑦)
115, 10eqsstri 3784 . . . . . . . 8 (𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
12 cononrel1 38419 . . . . . . . . 9 ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))) = ∅
1312, 8eqsstri 3784 . . . . . . . 8 ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
1411, 13unssi 3939 . . . . . . 7 ((𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ∪ ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋)))) ⊆ (𝑦𝑦)
154, 14eqsstri 3784 . . . . . 6 ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
16 id 22 . . . . . 6 ((𝑦𝑦) ⊆ 𝑦 → (𝑦𝑦) ⊆ 𝑦)
1715, 16syl5ss 3763 . . . . 5 ((𝑦𝑦) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ 𝑦)
18 ssun3 3929 . . . . 5 (((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋)))
193, 17, 183syl 18 . . . 4 ((𝑦𝑦) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋)))
20 id 22 . . . . . 6 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → 𝑥 = (𝑦 ∪ (𝑋𝑋)))
2120, 20coeq12d 5423 . . . . 5 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → (𝑥𝑥) = ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))))
2221, 20sseq12d 3783 . . . 4 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → ((𝑥𝑥) ⊆ 𝑥 ↔ ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋))))
2319, 22syl5ibr 236 . . 3 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → ((𝑦𝑦) ⊆ 𝑦 → (𝑥𝑥) ⊆ 𝑥))
2423adantl 467 . 2 ((𝑋𝑉𝑥 = (𝑦 ∪ (𝑋𝑋))) → ((𝑦𝑦) ⊆ 𝑦 → (𝑥𝑥) ⊆ 𝑥))
25 cnvco 5444 . . . . 5 (𝑥𝑥) = (𝑥𝑥)
26 cnvss 5431 . . . . 5 ((𝑥𝑥) ⊆ 𝑥(𝑥𝑥) ⊆ 𝑥)
2725, 26syl5eqssr 3799 . . . 4 ((𝑥𝑥) ⊆ 𝑥 → (𝑥𝑥) ⊆ 𝑥)
28 id 22 . . . . . 6 (𝑦 = 𝑥𝑦 = 𝑥)
2928, 28coeq12d 5423 . . . . 5 (𝑦 = 𝑥 → (𝑦𝑦) = (𝑥𝑥))
3029, 28sseq12d 3783 . . . 4 (𝑦 = 𝑥 → ((𝑦𝑦) ⊆ 𝑦 ↔ (𝑥𝑥) ⊆ 𝑥))
3127, 30syl5ibr 236 . . 3 (𝑦 = 𝑥 → ((𝑥𝑥) ⊆ 𝑥 → (𝑦𝑦) ⊆ 𝑦))
3231adantl 467 . 2 ((𝑋𝑉𝑦 = 𝑥) → ((𝑥𝑥) ⊆ 𝑥 → (𝑦𝑦) ⊆ 𝑦))
33 id 22 . . . 4 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → 𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
3433, 33coeq12d 5423 . . 3 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → (𝑥𝑥) = ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
3534, 33sseq12d 3783 . 2 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → ((𝑥𝑥) ⊆ 𝑥 ↔ ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
36 ssun1 3927 . . 3 𝑋 ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
3736a1i 11 . 2 (𝑋𝑉𝑋 ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
38 trclexlem 13936 . 2 (𝑋𝑉 → (𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∈ V)
39 coundir 5779 . . . . 5 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = ((𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ∪ ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
40 coundi 5778 . . . . . . 7 (𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = ((𝑋𝑋) ∪ (𝑋 ∘ (dom 𝑋 × ran 𝑋)))
41 cossxp 5800 . . . . . . . 8 (𝑋𝑋) ⊆ (dom 𝑋 × ran 𝑋)
42 cossxp 5800 . . . . . . . . 9 (𝑋 ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom (dom 𝑋 × ran 𝑋) × ran 𝑋)
43 dmxpss 5704 . . . . . . . . . 10 dom (dom 𝑋 × ran 𝑋) ⊆ dom 𝑋
44 xpss1 5267 . . . . . . . . . 10 (dom (dom 𝑋 × ran 𝑋) ⊆ dom 𝑋 → (dom (dom 𝑋 × ran 𝑋) × ran 𝑋) ⊆ (dom 𝑋 × ran 𝑋))
4543, 44ax-mp 5 . . . . . . . . 9 (dom (dom 𝑋 × ran 𝑋) × ran 𝑋) ⊆ (dom 𝑋 × ran 𝑋)
4642, 45sstri 3761 . . . . . . . 8 (𝑋 ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
4741, 46unssi 3939 . . . . . . 7 ((𝑋𝑋) ∪ (𝑋 ∘ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
4840, 47eqsstri 3784 . . . . . 6 (𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
49 coundi 5778 . . . . . . 7 ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = (((dom 𝑋 × ran 𝑋) ∘ 𝑋) ∪ ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋)))
50 cossxp 5800 . . . . . . . . 9 ((dom 𝑋 × ran 𝑋) ∘ 𝑋) ⊆ (dom 𝑋 × ran (dom 𝑋 × ran 𝑋))
51 rnxpss 5705 . . . . . . . . . 10 ran (dom 𝑋 × ran 𝑋) ⊆ ran 𝑋
52 xpss2 5268 . . . . . . . . . 10 (ran (dom 𝑋 × ran 𝑋) ⊆ ran 𝑋 → (dom 𝑋 × ran (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋))
5351, 52ax-mp 5 . . . . . . . . 9 (dom 𝑋 × ran (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
5450, 53sstri 3761 . . . . . . . 8 ((dom 𝑋 × ran 𝑋) ∘ 𝑋) ⊆ (dom 𝑋 × ran 𝑋)
55 xptrrel 13922 . . . . . . . 8 ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
5654, 55unssi 3939 . . . . . . 7 (((dom 𝑋 × ran 𝑋) ∘ 𝑋) ∪ ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
5749, 56eqsstri 3784 . . . . . 6 ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
5848, 57unssi 3939 . . . . 5 ((𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ∪ ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))) ⊆ (dom 𝑋 × ran 𝑋)
5939, 58eqsstri 3784 . . . 4 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
60 ssun2 3928 . . . 4 (dom 𝑋 × ran 𝑋) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
6159, 60sstri 3761 . . 3 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
6261a1i 11 . 2 (𝑋𝑉 → ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
6324, 32, 35, 37, 38, 62clcnvlem 38449 1 (𝑋𝑉 {𝑥 ∣ (𝑋𝑥 ∧ (𝑥𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑋𝑦 ∧ (𝑦𝑦) ⊆ 𝑦)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1631  wcel 2145  {cab 2757  cdif 3720  cun 3721  wss 3723  c0 4063   cint 4611   × cxp 5247  ccnv 5248  dom cdm 5249  ran crn 5250  ccom 5253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-int 4612  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-iota 5992  df-fun 6031  df-fv 6037  df-1st 7313  df-2nd 7314
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator