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 43195
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 5888 . . . . . 6 (𝑦𝑦) = (𝑦𝑦)
2 cnvss 5875 . . . . . 6 ((𝑦𝑦) ⊆ 𝑦(𝑦𝑦) ⊆ 𝑦)
31, 2eqsstrrid 4026 . . . . 5 ((𝑦𝑦) ⊆ 𝑦 → (𝑦𝑦) ⊆ 𝑦)
4 coundir 6254 . . . . . . 7 ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) = ((𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ∪ ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))))
5 coundi 6253 . . . . . . . . 9 (𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) = ((𝑦𝑦) ∪ (𝑦 ∘ (𝑋𝑋)))
6 ssid 3999 . . . . . . . . . 10 (𝑦𝑦) ⊆ (𝑦𝑦)
7 cononrel2 43164 . . . . . . . . . . 11 (𝑦 ∘ (𝑋𝑋)) = ∅
8 0ss 4398 . . . . . . . . . . 11 ∅ ⊆ (𝑦𝑦)
97, 8eqsstri 4011 . . . . . . . . . 10 (𝑦 ∘ (𝑋𝑋)) ⊆ (𝑦𝑦)
106, 9unssi 4183 . . . . . . . . 9 ((𝑦𝑦) ∪ (𝑦 ∘ (𝑋𝑋))) ⊆ (𝑦𝑦)
115, 10eqsstri 4011 . . . . . . . 8 (𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
12 cononrel1 43163 . . . . . . . . 9 ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))) = ∅
1312, 8eqsstri 4011 . . . . . . . 8 ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
1411, 13unssi 4183 . . . . . . 7 ((𝑦 ∘ (𝑦 ∪ (𝑋𝑋))) ∪ ((𝑋𝑋) ∘ (𝑦 ∪ (𝑋𝑋)))) ⊆ (𝑦𝑦)
154, 14eqsstri 4011 . . . . . 6 ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦𝑦)
16 id 22 . . . . . 6 ((𝑦𝑦) ⊆ 𝑦 → (𝑦𝑦) ⊆ 𝑦)
1715, 16sstrid 3988 . . . . 5 ((𝑦𝑦) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ 𝑦)
18 ssun3 4172 . . . . 5 (((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋)))
193, 17, 183syl 18 . . . 4 ((𝑦𝑦) ⊆ 𝑦 → ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋)))
20 id 22 . . . . . 6 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → 𝑥 = (𝑦 ∪ (𝑋𝑋)))
2120, 20coeq12d 5867 . . . . 5 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → (𝑥𝑥) = ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))))
2221, 20sseq12d 4010 . . . 4 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → ((𝑥𝑥) ⊆ 𝑥 ↔ ((𝑦 ∪ (𝑋𝑋)) ∘ (𝑦 ∪ (𝑋𝑋))) ⊆ (𝑦 ∪ (𝑋𝑋))))
2319, 22imbitrrid 245 . . 3 (𝑥 = (𝑦 ∪ (𝑋𝑋)) → ((𝑦𝑦) ⊆ 𝑦 → (𝑥𝑥) ⊆ 𝑥))
2423adantl 480 . 2 ((𝑋𝑉𝑥 = (𝑦 ∪ (𝑋𝑋))) → ((𝑦𝑦) ⊆ 𝑦 → (𝑥𝑥) ⊆ 𝑥))
25 cnvco 5888 . . . . 5 (𝑥𝑥) = (𝑥𝑥)
26 cnvss 5875 . . . . 5 ((𝑥𝑥) ⊆ 𝑥(𝑥𝑥) ⊆ 𝑥)
2725, 26eqsstrrid 4026 . . . 4 ((𝑥𝑥) ⊆ 𝑥 → (𝑥𝑥) ⊆ 𝑥)
28 id 22 . . . . . 6 (𝑦 = 𝑥𝑦 = 𝑥)
2928, 28coeq12d 5867 . . . . 5 (𝑦 = 𝑥 → (𝑦𝑦) = (𝑥𝑥))
3029, 28sseq12d 4010 . . . 4 (𝑦 = 𝑥 → ((𝑦𝑦) ⊆ 𝑦 ↔ (𝑥𝑥) ⊆ 𝑥))
3127, 30imbitrrid 245 . . 3 (𝑦 = 𝑥 → ((𝑥𝑥) ⊆ 𝑥 → (𝑦𝑦) ⊆ 𝑦))
3231adantl 480 . 2 ((𝑋𝑉𝑦 = 𝑥) → ((𝑥𝑥) ⊆ 𝑥 → (𝑦𝑦) ⊆ 𝑦))
33 id 22 . . . 4 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → 𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
3433, 33coeq12d 5867 . . 3 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → (𝑥𝑥) = ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
3534, 33sseq12d 4010 . 2 (𝑥 = (𝑋 ∪ (dom 𝑋 × ran 𝑋)) → ((𝑥𝑥) ⊆ 𝑥 ↔ ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
36 ssun1 4170 . . 3 𝑋 ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
3736a1i 11 . 2 (𝑋𝑉𝑋 ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
38 trclexlem 14977 . 2 (𝑋𝑉 → (𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∈ V)
39 coundir 6254 . . . . 5 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = ((𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ∪ ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))))
40 coundi 6253 . . . . . . 7 (𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = ((𝑋𝑋) ∪ (𝑋 ∘ (dom 𝑋 × ran 𝑋)))
41 cossxp 6278 . . . . . . . 8 (𝑋𝑋) ⊆ (dom 𝑋 × ran 𝑋)
42 cossxp 6278 . . . . . . . . 9 (𝑋 ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom (dom 𝑋 × ran 𝑋) × ran 𝑋)
43 dmxpss 6177 . . . . . . . . . 10 dom (dom 𝑋 × ran 𝑋) ⊆ dom 𝑋
44 xpss1 5697 . . . . . . . . . 10 (dom (dom 𝑋 × ran 𝑋) ⊆ dom 𝑋 → (dom (dom 𝑋 × ran 𝑋) × ran 𝑋) ⊆ (dom 𝑋 × ran 𝑋))
4543, 44ax-mp 5 . . . . . . . . 9 (dom (dom 𝑋 × ran 𝑋) × ran 𝑋) ⊆ (dom 𝑋 × ran 𝑋)
4642, 45sstri 3986 . . . . . . . 8 (𝑋 ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
4741, 46unssi 4183 . . . . . . 7 ((𝑋𝑋) ∪ (𝑋 ∘ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
4840, 47eqsstri 4011 . . . . . 6 (𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
49 coundi 6253 . . . . . . 7 ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) = (((dom 𝑋 × ran 𝑋) ∘ 𝑋) ∪ ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋)))
50 cossxp 6278 . . . . . . . . 9 ((dom 𝑋 × ran 𝑋) ∘ 𝑋) ⊆ (dom 𝑋 × ran (dom 𝑋 × ran 𝑋))
51 rnxpss 6178 . . . . . . . . . 10 ran (dom 𝑋 × ran 𝑋) ⊆ ran 𝑋
52 xpss2 5698 . . . . . . . . . 10 (ran (dom 𝑋 × ran 𝑋) ⊆ ran 𝑋 → (dom 𝑋 × ran (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋))
5351, 52ax-mp 5 . . . . . . . . 9 (dom 𝑋 × ran (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
5450, 53sstri 3986 . . . . . . . 8 ((dom 𝑋 × ran 𝑋) ∘ 𝑋) ⊆ (dom 𝑋 × ran 𝑋)
55 xptrrel 14963 . . . . . . . 8 ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋)) ⊆ (dom 𝑋 × ran 𝑋)
5654, 55unssi 4183 . . . . . . 7 (((dom 𝑋 × ran 𝑋) ∘ 𝑋) ∪ ((dom 𝑋 × ran 𝑋) ∘ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
5749, 56eqsstri 4011 . . . . . 6 ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
5848, 57unssi 4183 . . . . 5 ((𝑋 ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ∪ ((dom 𝑋 × ran 𝑋) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))) ⊆ (dom 𝑋 × ran 𝑋)
5939, 58eqsstri 4011 . . . 4 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (dom 𝑋 × ran 𝑋)
60 ssun2 4171 . . . 4 (dom 𝑋 × ran 𝑋) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
6159, 60sstri 3986 . . 3 ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋))
6261a1i 11 . 2 (𝑋𝑉 → ((𝑋 ∪ (dom 𝑋 × ran 𝑋)) ∘ (𝑋 ∪ (dom 𝑋 × ran 𝑋))) ⊆ (𝑋 ∪ (dom 𝑋 × ran 𝑋)))
6324, 32, 35, 37, 38, 62clcnvlem 43192 1 (𝑋𝑉 {𝑥 ∣ (𝑋𝑥 ∧ (𝑥𝑥) ⊆ 𝑥)} = {𝑦 ∣ (𝑋𝑦 ∧ (𝑦𝑦) ⊆ 𝑦)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wcel 2098  {cab 2702  cdif 3941  cun 3942  wss 3944  c0 4322   cint 4950   × cxp 5676  ccnv 5677  dom cdm 5678  ran crn 5679  ccom 5682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-iota 6501  df-fun 6551  df-fv 6557  df-1st 7994  df-2nd 7995
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator