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

Theorem iiner 6935
 Description: The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
Assertion
Ref Expression
iiner
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem iiner
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r19.2z 3677 . . . 4
2 errel 6873 . . . . . 6
3 df-rel 4844 . . . . . 6
42, 3sylib 189 . . . . 5
54reximi 2773 . . . 4
6 iinss 4102 . . . 4
71, 5, 63syl 19 . . 3
8 df-rel 4844 . . 3
97, 8sylibr 204 . 2
10 id 20 . . . . . . . . 9
1110ersymb 6878 . . . . . . . 8
1211biimpd 199 . . . . . . 7
13 df-br 4173 . . . . . . 7
14 df-br 4173 . . . . . . 7
1512, 13, 143imtr3g 261 . . . . . 6
1615ral2imi 2742 . . . . 5
1716adantl 453 . . . 4
18 df-br 4173 . . . . 5
19 opex 4387 . . . . . 6
20 eliin 4058 . . . . . 6
2119, 20ax-mp 8 . . . . 5
2218, 21bitri 241 . . . 4
23 df-br 4173 . . . . 5
24 opex 4387 . . . . . 6
25 eliin 4058 . . . . . 6
2624, 25ax-mp 8 . . . . 5
2723, 26bitri 241 . . . 4
2817, 22, 273imtr4g 262 . . 3
2928imp 419 . 2
30 r19.26 2798 . . . . 5
3110ertr 6879 . . . . . . . 8
32 df-br 4173 . . . . . . . . 9
3313, 32anbi12i 679 . . . . . . . 8
34 df-br 4173 . . . . . . . 8
3531, 33, 343imtr3g 261 . . . . . . 7
3635ral2imi 2742 . . . . . 6
3736adantl 453 . . . . 5
3830, 37syl5bir 210 . . . 4
39 df-br 4173 . . . . . 6
40 opex 4387 . . . . . . 7
41 eliin 4058 . . . . . . 7
4240, 41ax-mp 8 . . . . . 6
4339, 42bitri 241 . . . . 5
4422, 43anbi12i 679 . . . 4
45 df-br 4173 . . . . 5
46 opex 4387 . . . . . 6
47 eliin 4058 . . . . . 6
4846, 47ax-mp 8 . . . . 5
4945, 48bitri 241 . . . 4
5038, 44, 493imtr4g 262 . . 3
5150imp 419 . 2
52 simpl 444 . . . . . . . . . 10
53 simpr 448 . . . . . . . . . 10
5452, 53erref 6884 . . . . . . . . 9
55 df-br 4173 . . . . . . . . 9
5654, 55sylib 189 . . . . . . . 8
5756expcom 425 . . . . . . 7
5857ralimdv 2745 . . . . . 6
5958com12 29 . . . . 5
6059adantl 453 . . . 4
61 r19.26 2798 . . . . . 6
62 r19.2z 3677 . . . . . . . 8
63 vex 2919 . . . . . . . . . . 11
6463, 63opeldm 5032 . . . . . . . . . 10
65 erdm 6874 . . . . . . . . . . . 12
6665eleq2d 2471 . . . . . . . . . . 11
6766biimpa 471 . . . . . . . . . 10
6864, 67sylan2 461 . . . . . . . . 9
6968rexlimivw 2786 . . . . . . . 8
7062, 69syl 16 . . . . . . 7
7170ex 424 . . . . . 6
7261, 71syl5bir 210 . . . . 5
7372expdimp 427 . . . 4
7460, 73impbid 184 . . 3
75 df-br 4173 . . . 4
76 opex 4387 . . . . 5
77 eliin 4058 . . . . 5
7876, 77ax-mp 8 . . . 4
7975, 78bitri 241 . . 3
8074, 79syl6bbr 255 . 2
819, 29, 51, 80iserd 6890 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wcel 1721   wne 2567  wral 2666  wrex 2667  cvv 2916   wss 3280  c0 3588  cop 3777  ciin 4054   class class class wbr 4172   cxp 4835   cdm 4837   wrel 4842   wer 6861 This theorem is referenced by:  riiner  6936  efger  15305 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-iin 4056  df-br 4173  df-opab 4227  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-er 6864
 Copyright terms: Public domain W3C validator