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 39471
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 5642 . . . . . 6 (𝑦𝑦) = (𝑦𝑦)
2 cnvss 5629 . . . . . 6 ((𝑦𝑦) ⊆ 𝑦(𝑦𝑦) ⊆ 𝑦)
31, 2eqsstrrid 3937 . . . . 5 ((𝑦𝑦) ⊆ 𝑦 → (𝑦𝑦) ⊆ 𝑦)
4 coundir 5976 . . . . . . 7 ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) = ((𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ∪ ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))))
5 coundi 5975 . . . . . . . . 9 (𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) = ((𝑦𝑦) ∪ (𝑦 ∘ (𝑋𝑋)))
6 ssid 3910 . . . . . . . . . 10 (𝑦𝑦) ⊆ (𝑦𝑦)
7 cononrel2 39440 . . . . . . . . . . 11 (𝑦 ∘ (𝑋𝑋)) = ∅
8 0ss 4270 . . . . . . . . . . 11 ∅ ⊆ (𝑦𝑦)
97, 8eqsstri 3922 . . . . . . . . . 10 (𝑦 ∘ (𝑋𝑋)) ⊆ (𝑦𝑦)
106, 9unssi 4082 . . . . . . . . 9 ((𝑦𝑦) ∪ (𝑦 ∘ (𝑋𝑋))) ⊆ (𝑦𝑦)
115, 10eqsstri 3922 . . . . . . . 8 (𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
12 cononrel1 39439 . . . . . . . . 9 ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))) = ∅
1312, 8eqsstri 3922 . . . . . . . 8 ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
1411, 13unssi 4082 . . . . . . 7 ((𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ∪ ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋)))) ⊆ (𝑦𝑦)
154, 14eqsstri 3922 . . . . . 6 ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
16 id 22 . . . . . 6 ((𝑦𝑦) ⊆ 𝑦 → (𝑦𝑦) ⊆ 𝑦)
1715, 16syl5ss 3900 . . . . 5 ((𝑦𝑦) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ 𝑦)
18 ssun3 4071 . . . . 5 (((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋)))
193, 17, 183syl 18 . . . 4 ((𝑦𝑦) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋)))
20 id 22 . . . . . 6 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → 𝑥 = (𝑦 ∪ (𝑋𝑋)))
2120, 20coeq12d 5621 . . . . 5 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → (𝑥𝑥) = ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))))
2221, 20sseq12d 3921 . . . 4 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → ((𝑥𝑥) ⊆ 𝑥 ↔ ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋))))
2319, 22syl5ibr 247 . . 3 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → ((𝑦𝑦) ⊆ 𝑦 → (𝑥𝑥) ⊆ 𝑥))
2423adantl 482 . 2 ((𝑋𝑉𝑥 = (𝑦 ∪ (𝑋𝑋))) → ((𝑦𝑦) ⊆ 𝑦 → (𝑥𝑥) ⊆ 𝑥))
25 cnvco 5642 . . . . 5 (𝑥𝑥) = (𝑥𝑥)
26 cnvss 5629 . . . . 5 ((𝑥𝑥) ⊆ 𝑥(𝑥𝑥) ⊆ 𝑥)
2725, 26eqsstrrid 3937 . . . 4 ((𝑥𝑥) ⊆ 𝑥 → (𝑥𝑥) ⊆ 𝑥)
28 id 22 . . . . . 6 (𝑦 = 𝑥𝑦 = 𝑥)
2928, 28coeq12d 5621 . . . . 5 (𝑦 = 𝑥 → (𝑦𝑦) = (𝑥𝑥))
3029, 28sseq12d 3921 . . . 4 (𝑦 = 𝑥 → ((𝑦𝑦) ⊆ 𝑦 ↔ (𝑥𝑥) ⊆ 𝑥))
3127, 30syl5ibr 247 . . 3 (𝑦 = 𝑥 → ((𝑥𝑥) ⊆ 𝑥 → (𝑦𝑦) ⊆ 𝑦))
3231adantl 482 . 2 ((𝑋𝑉𝑦 = 𝑥) → ((𝑥𝑥) ⊆ 𝑥 → (𝑦𝑦) ⊆ 𝑦))
33 id 22 . . . 4 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → 𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
3433, 33coeq12d 5621 . . 3 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → (𝑥𝑥) = ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
3534, 33sseq12d 3921 . 2 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → ((𝑥𝑥) ⊆ 𝑥 ↔ ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
36 ssun1 4069 . . 3 𝑋 ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
3736a1i 11 . 2 (𝑋𝑉𝑋 ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
38 trclexlem 14188 . 2 (𝑋𝑉 → (𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∈ V)
39 coundir 5976 . . . . 5 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = ((𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ∪ ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
40 coundi 5975 . . . . . . 7 (𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = ((𝑋𝑋) ∪ (𝑋 ∘ (dom 𝑋 × ran 𝑋)))
41 cossxp 5998 . . . . . . . 8 (𝑋𝑋) ⊆ (dom 𝑋 × ran 𝑋)
42 cossxp 5998 . . . . . . . . 9 (𝑋 ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom (dom 𝑋 × ran 𝑋) × ran 𝑋)
43 dmxpss 5904 . . . . . . . . . 10 dom (dom 𝑋 × ran 𝑋) ⊆ dom 𝑋
44 xpss1 5462 . . . . . . . . . 10 (dom (dom 𝑋 × ran 𝑋) ⊆ dom 𝑋 → (dom (dom 𝑋 × ran 𝑋) × ran 𝑋) ⊆ (dom 𝑋 × ran 𝑋))
4543, 44ax-mp 5 . . . . . . . . 9 (dom (dom 𝑋 × ran 𝑋) × ran 𝑋) ⊆ (dom 𝑋 × ran 𝑋)
4642, 45sstri 3898 . . . . . . . 8 (𝑋 ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
4741, 46unssi 4082 . . . . . . 7 ((𝑋𝑋) ∪ (𝑋 ∘ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
4840, 47eqsstri 3922 . . . . . 6 (𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
49 coundi 5975 . . . . . . 7 ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = (((dom 𝑋 × ran 𝑋) ∘ 𝑋) ∪ ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋)))
50 cossxp 5998 . . . . . . . . 9 ((dom 𝑋 × ran 𝑋) ∘ 𝑋) ⊆ (dom 𝑋 × ran (dom 𝑋 × ran 𝑋))
51 rnxpss 5905 . . . . . . . . . 10 ran (dom 𝑋 × ran 𝑋) ⊆ ran 𝑋
52 xpss2 5463 . . . . . . . . . 10 (ran (dom 𝑋 × ran 𝑋) ⊆ ran 𝑋 → (dom 𝑋 × ran (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋))
5351, 52ax-mp 5 . . . . . . . . 9 (dom 𝑋 × ran (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
5450, 53sstri 3898 . . . . . . . 8 ((dom 𝑋 × ran 𝑋) ∘ 𝑋) ⊆ (dom 𝑋 × ran 𝑋)
55 xptrrel 14174 . . . . . . . 8 ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
5654, 55unssi 4082 . . . . . . 7 (((dom 𝑋 × ran 𝑋) ∘ 𝑋) ∪ ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
5749, 56eqsstri 3922 . . . . . 6 ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
5848, 57unssi 4082 . . . . 5 ((𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ∪ ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))) ⊆ (dom 𝑋 × ran 𝑋)
5939, 58eqsstri 3922 . . . 4 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
60 ssun2 4070 . . . 4 (dom 𝑋 × ran 𝑋) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
6159, 60sstri 3898 . . 3 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
6261a1i 11 . 2 (𝑋𝑉 → ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
6324, 32, 35, 37, 38, 62clcnvlem 39468 1 (𝑋𝑉 {𝑥 ∣ (𝑋𝑥 ∧ (𝑥𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑋𝑦 ∧ (𝑦𝑦) ⊆ 𝑦)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1522  wcel 2081  {cab 2775  cdif 3856  cun 3857  wss 3859  c0 4211   cint 4782   × cxp 5441  ccnv 5442  dom cdm 5443  ran crn 5444  ccom 5447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-int 4783  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-iota 6189  df-fun 6227  df-fv 6233  df-1st 7545  df-2nd 7546
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator