Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  disjdsct Structured version   Unicode version

Theorem disjdsct 28270
 Description: A disjoint collection is distinct, i.e. each set in this collection is different of all others, provided that it does not contain the empty set This can be expressed as "the converse of the mapping function is a function", or "the mapping function is single-rooted". (Cf. funcnv 5657) (Contributed by Thierry Arnoux, 28-Feb-2017.)
Hypotheses
Ref Expression
disjdsct.0
disjdsct.1
disjdsct.2
disjdsct.3 Disj
Assertion
Ref Expression
disjdsct
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem disjdsct
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 disjdsct.3 . . . . . . . 8 Disj
2 disjdsct.1 . . . . . . . . 9
32disjorsf 28177 . . . . . . . 8 Disj
41, 3sylib 199 . . . . . . 7
54r19.21bi 2794 . . . . . 6
65r19.21bi 2794 . . . . 5
7 simpr3 1013 . . . . . . . . 9
8 disjdsct.2 . . . . . . . . . . . . 13
9 eldifsni 4123 . . . . . . . . . . . . 13
108, 9syl 17 . . . . . . . . . . . 12
1110sbimi 1792 . . . . . . . . . . 11
12 sban 2193 . . . . . . . . . . . 12
13 disjdsct.0 . . . . . . . . . . . . . 14
1413sbf 2174 . . . . . . . . . . . . 13
152clelsb3f 28099 . . . . . . . . . . . . 13
1614, 15anbi12i 701 . . . . . . . . . . . 12
1712, 16bitri 252 . . . . . . . . . . 11
18 sbsbc 3303 . . . . . . . . . . . 12
19 sbcne12 3803 . . . . . . . . . . . 12
20 csb0 3799 . . . . . . . . . . . . 13
2120neeq2i 2711 . . . . . . . . . . . 12
2218, 19, 213bitri 274 . . . . . . . . . . 11
2311, 17, 223imtr3i 268 . . . . . . . . . 10
24233ad2antr1 1170 . . . . . . . . 9
25 disj3 3837 . . . . . . . . . . . . 13
2625biimpi 197 . . . . . . . . . . . 12
2726neeq1d 2701 . . . . . . . . . . 11
2827biimpa 486 . . . . . . . . . 10
29 difn0 3852 . . . . . . . . . 10
3028, 29syl 17 . . . . . . . . 9
317, 24, 30syl2anc 665 . . . . . . . 8
32313anassrs 1228 . . . . . . 7
3332ex 435 . . . . . 6
3433orim2d 848 . . . . 5
356, 34mpd 15 . . . 4
3635ralrimiva 2839 . . 3
3736ralrimiva 2839 . 2
38 nfmpt1 4510 . . 3
39 eqid 2422 . . 3
4013, 2, 38, 39, 8funcnv4mpt 28260 . 2
4137, 40mpbird 235 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 369   wa 370   w3a 982   wceq 1437  wnf 1663  wsb 1786   wcel 1868  wnfc 2570   wne 2618  wral 2775  wsbc 3299  csb 3395   cdif 3433   cin 3435  c0 3761  csn 3996  Disj wdisj 4391   cmpt 4479  ccnv 4848   wfun 5591 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pr 4656 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-disj 4392  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-fv 5605 This theorem is referenced by:  esumrnmpt  28866  measvunilem  29027
 Copyright terms: Public domain W3C validator