Users' Mathboxes 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  |-  F/ x ph
disjdsct.1  |-  F/_ x A
disjdsct.2  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  ( V  \  { (/)
} ) )
disjdsct.3  |-  ( ph  -> Disj  x  e.  A  B
)
Assertion
Ref Expression
disjdsct  |-  ( ph  ->  Fun  `' ( x  e.  A  |->  B ) )
Distinct variable group:    x, V
Allowed substitution hints:    ph( x)    A( x)    B( x)

Proof of Theorem disjdsct
Dummy variables  i 
j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 disjdsct.3 . . . . . . . 8  |-  ( ph  -> Disj  x  e.  A  B
)
2 disjdsct.1 . . . . . . . . 9  |-  F/_ x A
32disjorsf 28177 . . . . . . . 8  |-  (Disj  x  e.  A  B  <->  A. i  e.  A  A. j  e.  A  ( i  =  j  \/  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )
41, 3sylib 199 . . . . . . 7  |-  ( ph  ->  A. i  e.  A  A. j  e.  A  ( i  =  j  \/  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )
54r19.21bi 2794 . . . . . 6  |-  ( (
ph  /\  i  e.  A )  ->  A. j  e.  A  ( i  =  j  \/  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )
65r19.21bi 2794 . . . . 5  |-  ( ( ( ph  /\  i  e.  A )  /\  j  e.  A )  ->  (
i  =  j  \/  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )
7 simpr3 1013 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  A  /\  j  e.  A  /\  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )  -> 
( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) )
8 disjdsct.2 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  ( V  \  { (/)
} ) )
9 eldifsni 4123 . . . . . . . . . . . . 13  |-  ( B  e.  ( V  \  { (/) } )  ->  B  =/=  (/) )
108, 9syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  B  =/=  (/) )
1110sbimi 1792 . . . . . . . . . . 11  |-  ( [ i  /  x ]
( ph  /\  x  e.  A )  ->  [ i  /  x ] B  =/=  (/) )
12 sban 2193 . . . . . . . . . . . 12  |-  ( [ i  /  x ]
( ph  /\  x  e.  A )  <->  ( [
i  /  x ] ph  /\  [ i  /  x ] x  e.  A
) )
13 disjdsct.0 . . . . . . . . . . . . . 14  |-  F/ x ph
1413sbf 2174 . . . . . . . . . . . . 13  |-  ( [ i  /  x ] ph 
<-> 
ph )
152clelsb3f 28099 . . . . . . . . . . . . 13  |-  ( [ i  /  x ]
x  e.  A  <->  i  e.  A )
1614, 15anbi12i 701 . . . . . . . . . . . 12  |-  ( ( [ i  /  x ] ph  /\  [ i  /  x ] x  e.  A )  <->  ( ph  /\  i  e.  A ) )
1712, 16bitri 252 . . . . . . . . . . 11  |-  ( [ i  /  x ]
( ph  /\  x  e.  A )  <->  ( ph  /\  i  e.  A ) )
18 sbsbc 3303 . . . . . . . . . . . 12  |-  ( [ i  /  x ] B  =/=  (/)  <->  [. i  /  x ]. B  =/=  (/) )
19 sbcne12 3803 . . . . . . . . . . . 12  |-  ( [. i  /  x ]. B  =/=  (/)  <->  [_ i  /  x ]_ B  =/=  [_ i  /  x ]_ (/) )
20 csb0 3799 . . . . . . . . . . . . 13  |-  [_ i  /  x ]_ (/)  =  (/)
2120neeq2i 2711 . . . . . . . . . . . 12  |-  ( [_ i  /  x ]_ B  =/=  [_ i  /  x ]_ (/)  <->  [_ i  /  x ]_ B  =/=  (/) )
2218, 19, 213bitri 274 . . . . . . . . . . 11  |-  ( [ i  /  x ] B  =/=  (/)  <->  [_ i  /  x ]_ B  =/=  (/) )
2311, 17, 223imtr3i 268 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  A )  ->  [_ i  /  x ]_ B  =/=  (/) )
24233ad2antr1 1170 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  A  /\  j  e.  A  /\  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )  ->  [_ i  /  x ]_ B  =/=  (/) )
25 disj3 3837 . . . . . . . . . . . . 13  |-  ( (
[_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  <->  [_ i  /  x ]_ B  =  ( [_ i  /  x ]_ B  \  [_ j  /  x ]_ B ) )
2625biimpi 197 . . . . . . . . . . . 12  |-  ( (
[_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  ->  [_ i  /  x ]_ B  =  ( [_ i  /  x ]_ B  \  [_ j  /  x ]_ B ) )
2726neeq1d 2701 . . . . . . . . . . 11  |-  ( (
[_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  ->  ( [_ i  /  x ]_ B  =/=  (/)  <->  ( [_ i  /  x ]_ B  \  [_ j  /  x ]_ B )  =/=  (/) ) )
2827biimpa 486 . . . . . . . . . 10  |-  ( ( ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  /\  [_ i  /  x ]_ B  =/=  (/) )  ->  ( [_ i  /  x ]_ B  \ 
[_ j  /  x ]_ B )  =/=  (/) )
29 difn0 3852 . . . . . . . . . 10  |-  ( (
[_ i  /  x ]_ B  \  [_ j  /  x ]_ B )  =/=  (/)  ->  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B
)
3028, 29syl 17 . . . . . . . . 9  |-  ( ( ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  /\  [_ i  /  x ]_ B  =/=  (/) )  ->  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B )
317, 24, 30syl2anc 665 . . . . . . . 8  |-  ( (
ph  /\  ( i  e.  A  /\  j  e.  A  /\  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )  ->  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B )
32313anassrs 1228 . . . . . . 7  |-  ( ( ( ( ph  /\  i  e.  A )  /\  j  e.  A
)  /\  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) )  ->  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B )
3332ex 435 . . . . . 6  |-  ( ( ( ph  /\  i  e.  A )  /\  j  e.  A )  ->  (
( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  ->  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B ) )
3433orim2d 848 . . . . 5  |-  ( ( ( ph  /\  i  e.  A )  /\  j  e.  A )  ->  (
( i  =  j  \/  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) )  ->  ( i  =  j  \/  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B ) ) )
356, 34mpd 15 . . . 4  |-  ( ( ( ph  /\  i  e.  A )  /\  j  e.  A )  ->  (
i  =  j  \/ 
[_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B ) )
3635ralrimiva 2839 . . 3  |-  ( (
ph  /\  i  e.  A )  ->  A. j  e.  A  ( i  =  j  \/  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B ) )
3736ralrimiva 2839 . 2  |-  ( ph  ->  A. i  e.  A  A. j  e.  A  ( i  =  j  \/  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B
) )
38 nfmpt1 4510 . . 3  |-  F/_ x
( x  e.  A  |->  B )
39 eqid 2422 . . 3  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
4013, 2, 38, 39, 8funcnv4mpt 28260 . 2  |-  ( ph  ->  ( Fun  `' ( x  e.  A  |->  B )  <->  A. i  e.  A  A. j  e.  A  ( i  =  j  \/  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B
) ) )
4137, 40mpbird 235 1  |-  ( ph  ->  Fun  `' ( x  e.  A  |->  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437   F/wnf 1663   [wsb 1786    e. wcel 1868   F/_wnfc 2570    =/= wne 2618   A.wral 2775   [.wsbc 3299   [_csb 3395    \ cdif 3433    i^i cin 3435   (/)c0 3761   {csn 3996  Disj wdisj 4391    |-> cmpt 4479   `'ccnv 4848   Fun 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