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

Theorem disjdsct 27390
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 5635) (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 27310 . . . . . . . 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 196 . . . . . . 7  |-  ( ph  ->  A. i  e.  A  A. j  e.  A  ( i  =  j  \/  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )
54r19.21bi 2810 . . . . . 6  |-  ( (
ph  /\  i  e.  A )  ->  A. j  e.  A  ( i  =  j  \/  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )
65r19.21bi 2810 . . . . 5  |-  ( ( ( ph  /\  i  e.  A )  /\  j  e.  A )  ->  (
i  =  j  \/  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )
7 simpr3 1003 . . . . . . . . 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 4138 . . . . . . . . . . . . 13  |-  ( B  e.  ( V  \  { (/) } )  ->  B  =/=  (/) )
108, 9syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  B  =/=  (/) )
1110sbimi 1730 . . . . . . . . . . 11  |-  ( [ i  /  x ]
( ph  /\  x  e.  A )  ->  [ i  /  x ] B  =/=  (/) )
12 sban 2124 . . . . . . . . . . . 12  |-  ( [ i  /  x ]
( ph  /\  x  e.  A )  <->  ( [
i  /  x ] ph  /\  [ i  /  x ] x  e.  A
) )
13 disjdsct.0 . . . . . . . . . . . . . 14  |-  F/ x ph
1413sbf 2105 . . . . . . . . . . . . 13  |-  ( [ i  /  x ] ph 
<-> 
ph )
152clelsb3f 27248 . . . . . . . . . . . . 13  |-  ( [ i  /  x ]
x  e.  A  <->  i  e.  A )
1614, 15anbi12i 697 . . . . . . . . . . . 12  |-  ( ( [ i  /  x ] ph  /\  [ i  /  x ] x  e.  A )  <->  ( ph  /\  i  e.  A ) )
1712, 16bitri 249 . . . . . . . . . . 11  |-  ( [ i  /  x ]
( ph  /\  x  e.  A )  <->  ( ph  /\  i  e.  A ) )
18 sbsbc 3315 . . . . . . . . . . . 12  |-  ( [ i  /  x ] B  =/=  (/)  <->  [. i  /  x ]. B  =/=  (/) )
19 sbcne12 3810 . . . . . . . . . . . 12  |-  ( [. i  /  x ]. B  =/=  (/)  <->  [_ i  /  x ]_ B  =/=  [_ i  /  x ]_ (/) )
20 csb0 3805 . . . . . . . . . . . . 13  |-  [_ i  /  x ]_ (/)  =  (/)
2120neeq2i 2728 . . . . . . . . . . . 12  |-  ( [_ i  /  x ]_ B  =/=  [_ i  /  x ]_ (/)  <->  [_ i  /  x ]_ B  =/=  (/) )
2218, 19, 213bitri 271 . . . . . . . . . . 11  |-  ( [ i  /  x ] B  =/=  (/)  <->  [_ i  /  x ]_ B  =/=  (/) )
2311, 17, 223imtr3i 265 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  A )  ->  [_ i  /  x ]_ B  =/=  (/) )
24233ad2antr1 1160 . . . . . . . . 9  |-  ( (
ph  /\  ( i  e.  A  /\  j  e.  A  /\  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )  ->  [_ i  /  x ]_ B  =/=  (/) )
25 disj3 3854 . . . . . . . . . . . . 13  |-  ( (
[_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  <->  [_ i  /  x ]_ B  =  ( [_ i  /  x ]_ B  \  [_ j  /  x ]_ B ) )
2625biimpi 194 . . . . . . . . . . . 12  |-  ( (
[_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  ->  [_ i  /  x ]_ B  =  ( [_ i  /  x ]_ B  \  [_ j  /  x ]_ B ) )
2726neeq1d 2718 . . . . . . . . . . 11  |-  ( (
[_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  ->  ( [_ i  /  x ]_ B  =/=  (/)  <->  ( [_ i  /  x ]_ B  \  [_ j  /  x ]_ B )  =/=  (/) ) )
2827biimpa 484 . . . . . . . . . 10  |-  ( ( ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  /\  [_ i  /  x ]_ B  =/=  (/) )  ->  ( [_ i  /  x ]_ B  \ 
[_ j  /  x ]_ B )  =/=  (/) )
29 difneqnul 27284 . . . . . . . . . 10  |-  ( (
[_ i  /  x ]_ B  \  [_ j  /  x ]_ B )  =/=  (/)  ->  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B
)
3028, 29syl 16 . . . . . . . . 9  |-  ( ( ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  /\  [_ i  /  x ]_ B  =/=  (/) )  ->  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B )
317, 24, 30syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  ( i  e.  A  /\  j  e.  A  /\  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )  ->  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B )
32313anassrs 1217 . . . . . . 7  |-  ( ( ( ( ph  /\  i  e.  A )  /\  j  e.  A
)  /\  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) )  ->  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B )
3332ex 434 . . . . . 6  |-  ( ( ( ph  /\  i  e.  A )  /\  j  e.  A )  ->  (
( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/)  ->  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B ) )
3433orim2d 838 . . . . 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 2855 . . 3  |-  ( (
ph  /\  i  e.  A )  ->  A. j  e.  A  ( i  =  j  \/  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B ) )
3736ralrimiva 2855 . 2  |-  ( ph  ->  A. i  e.  A  A. j  e.  A  ( i  =  j  \/  [_ i  /  x ]_ B  =/=  [_ j  /  x ]_ B
) )
38 nfmpt1 4523 . . 3  |-  F/_ x
( x  e.  A  |->  B )
39 eqid 2441 . . 3  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
4013, 2, 38, 39, 8funcnv4mpt 27381 . 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 232 1  |-  ( ph  ->  Fun  `' ( x  e.  A  |->  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    /\ wa 369    /\ w3a 972    = wceq 1381   F/wnf 1601   [wsb 1724    e. wcel 1802   F/_wnfc 2589    =/= wne 2636   A.wral 2791   [.wsbc 3311   [_csb 3418    \ cdif 3456    i^i cin 3458   (/)c0 3768   {csn 4011  Disj wdisj 4404    |-> cmpt 4492   `'ccnv 4985   Fun wfun 5569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pr 4673
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-uni 4232  df-disj 4405  df-br 4435  df-opab 4493  df-mpt 4494  df-id 4782  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-fv 5583
This theorem is referenced by:  measvunilem  28053
  Copyright terms: Public domain W3C validator