Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  trclublem Structured version   Visualization version   Unicode version

Theorem trclublem 13071
 Description: If a relation exists then the class of transitive relations which are supersets of that relation is not empty. (Contributed by RP, 28-Apr-2020.)
Assertion
Ref Expression
trclublem
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem trclublem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 trclexlem 13070 . 2
2 ssun1 3599 . . 3
3 relcnv 5210 . . . . . . . . . . . . . 14
4 relssdmrn 5359 . . . . . . . . . . . . . 14
53, 4ax-mp 5 . . . . . . . . . . . . 13
6 ssequn1 3606 . . . . . . . . . . . . 13
75, 6mpbi 212 . . . . . . . . . . . 12
8 cnvun 5244 . . . . . . . . . . . . 13
9 cnvxp 5257 . . . . . . . . . . . . . . 15
10 df-rn 4848 . . . . . . . . . . . . . . . 16
11 dfdm4 5030 . . . . . . . . . . . . . . . 16
1210, 11xpeq12i 4859 . . . . . . . . . . . . . . 15
139, 12eqtri 2475 . . . . . . . . . . . . . 14
1413uneq2i 3587 . . . . . . . . . . . . 13
158, 14eqtri 2475 . . . . . . . . . . . 12
167, 15, 133eqtr4i 2485 . . . . . . . . . . 11
1716breqi 4411 . . . . . . . . . 10
18 vex 3050 . . . . . . . . . . 11
19 vex 3050 . . . . . . . . . . 11
2018, 19brcnv 5020 . . . . . . . . . 10
2118, 19brcnv 5020 . . . . . . . . . 10
2217, 20, 213bitr3i 279 . . . . . . . . 9
2316breqi 4411 . . . . . . . . . 10
24 vex 3050 . . . . . . . . . . 11
2524, 18brcnv 5020 . . . . . . . . . 10
2624, 18brcnv 5020 . . . . . . . . . 10
2723, 25, 263bitr3i 279 . . . . . . . . 9
2822, 27anbi12i 704 . . . . . . . 8
2928biimpi 198 . . . . . . 7
3029eximi 1709 . . . . . 6
3130ssopab2i 4732 . . . . 5
32 df-co 4846 . . . . 5
33 df-co 4846 . . . . 5
3431, 32, 333sstr4i 3473 . . . 4
35 xptrrel 13056 . . . . 5
36 ssun2 3600 . . . . 5
3735, 36sstri 3443 . . . 4
3834, 37sstri 3443 . . 3
39 trcleq2lem 13067 . . . . 5
4039elabg 3188 . . . 4
4140biimprd 227 . . 3
422, 38, 41mp2ani 685 . 2
431, 42syl 17 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371   wceq 1446  wex 1665   wcel 1889  cab 2439  cvv 3047   cun 3404   wss 3406   class class class wbr 4405  copab 4463   cxp 4835  ccnv 4836   cdm 4837   crn 4838   ccom 4841   wrel 4842 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849 This theorem is referenced by:  trclubi  13072  trclubgi  13073  trclub  13074  trclubg  13075
 Copyright terms: Public domain W3C validator