Metamath Proof Explorer

Theorem disjdsct

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 ) (Contributed by Thierry Arnoux, 28-Feb-2017)

Ref Expression
Hypotheses 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 disjdsct 
|- ( ph -> Fun `' ( x e. A |-> B ) )

Proof

Step Hyp Ref Expression
1 disjdsct.0 
 |-  F/ x ph
2 disjdsct.1 
 |-  F/_ x A
3 disjdsct.2 
 |-  ( ( ph /\ x e. A ) -> B e. ( V \ { (/) } ) )
4 disjdsct.3 
 |-  ( ph -> Disj_ x e. A B )
5 2 disjorsf 
 |-  ( Disj_ x e. A B <-> A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
6 4 5 sylib 
 |-  ( ph -> A. i e. A A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
7 6 r19.21bi 
 |-  ( ( ph /\ i e. A ) -> A. j e. A ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
8 7 r19.21bi 
 |-  ( ( ( ph /\ i e. A ) /\ j e. A ) -> ( i = j \/ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) )
9 simpr3 
 |-  ( ( ph /\ ( i e. A /\ j e. A /\ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) -> ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) )
10 eldifsni 
 |-  ( B e. ( V \ { (/) } ) -> B =/= (/) )
11 3 10 syl 
 |-  ( ( ph /\ x e. A ) -> B =/= (/) )
12 11 sbimi 
 |-  ( [ i / x ] ( ph /\ x e. A ) -> [ i / x ] B =/= (/) )
13 sban 
 |-  ( [ i / x ] ( ph /\ x e. A ) <-> ( [ i / x ] ph /\ [ i / x ] x e. A ) )
14 1 sbf 
 |-  ( [ i / x ] ph <-> ph )
15 2 clelsb3fw 
 |-  ( [ i / x ] x e. A <-> i e. A )
16 14 15 anbi12i 
 |-  ( ( [ i / x ] ph /\ [ i / x ] x e. A ) <-> ( ph /\ i e. A ) )
17 13 16 bitri 
 |-  ( [ i / x ] ( ph /\ x e. A ) <-> ( ph /\ i e. A ) )
18 sbsbc 
 |-  ( [ i / x ] B =/= (/) <-> [. i / x ]. B =/= (/) )
19 sbcne12 
 |-  ( [. i / x ]. B =/= (/) <-> [_ i / x ]_ B =/= [_ i / x ]_ (/) )
20 csb0 
 |-  [_ i / x ]_ (/) = (/)
21 20 neeq2i 
 |-  ( [_ i / x ]_ B =/= [_ i / x ]_ (/) <-> [_ i / x ]_ B =/= (/) )
22 18 19 21 3bitri 
 |-  ( [ i / x ] B =/= (/) <-> [_ i / x ]_ B =/= (/) )
23 12 17 22 3imtr3i 
 |-  ( ( ph /\ i e. A ) -> [_ i / x ]_ B =/= (/) )
24 23 3ad2antr1 
 |-  ( ( ph /\ ( i e. A /\ j e. A /\ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) -> [_ i / x ]_ B =/= (/) )
25 disj3 
 |-  ( ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) <-> [_ i / x ]_ B = ( [_ i / x ]_ B \ [_ j / x ]_ B ) )
26 25 biimpi 
 |-  ( ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) -> [_ i / x ]_ B = ( [_ i / x ]_ B \ [_ j / x ]_ B ) )
27 26 neeq1d 
 |-  ( ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) -> ( [_ i / x ]_ B =/= (/) <-> ( [_ i / x ]_ B \ [_ j / x ]_ B ) =/= (/) ) )
28 27 biimpa 
 |-  ( ( ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) /\ [_ i / x ]_ B =/= (/) ) -> ( [_ i / x ]_ B \ [_ j / x ]_ B ) =/= (/) )
29 difn0 
 |-  ( ( [_ i / x ]_ B \ [_ j / x ]_ B ) =/= (/) -> [_ i / x ]_ B =/= [_ j / x ]_ B )
30 28 29 syl 
 |-  ( ( ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) /\ [_ i / x ]_ B =/= (/) ) -> [_ i / x ]_ B =/= [_ j / x ]_ B )
31 9 24 30 syl2anc 
 |-  ( ( ph /\ ( i e. A /\ j e. A /\ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) ) -> [_ i / x ]_ B =/= [_ j / x ]_ B )
32 31 3anassrs 
 |-  ( ( ( ( ph /\ i e. A ) /\ j e. A ) /\ ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) ) -> [_ i / x ]_ B =/= [_ j / x ]_ B )
33 32 ex 
 |-  ( ( ( ph /\ i e. A ) /\ j e. A ) -> ( ( [_ i / x ]_ B i^i [_ j / x ]_ B ) = (/) -> [_ i / x ]_ B =/= [_ j / x ]_ B ) )
34 33 orim2d 
 |-  ( ( ( 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 ) ) )
35 8 34 mpd 
 |-  ( ( ( ph /\ i e. A ) /\ j e. A ) -> ( i = j \/ [_ i / x ]_ B =/= [_ j / x ]_ B ) )
36 35 ralrimiva 
 |-  ( ( ph /\ i e. A ) -> A. j e. A ( i = j \/ [_ i / x ]_ B =/= [_ j / x ]_ B ) )
37 36 ralrimiva 
 |-  ( ph -> A. i e. A A. j e. A ( i = j \/ [_ i / x ]_ B =/= [_ j / x ]_ B ) )
38 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
39 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
40 1 2 38 39 3 funcnv4mpt 
 |-  ( ph -> ( Fun `' ( x e. A |-> B ) <-> A. i e. A A. j e. A ( i = j \/ [_ i / x ]_ B =/= [_ j / x ]_ B ) ) )
41 37 40 mpbird 
 |-  ( ph -> Fun `' ( x e. A |-> B ) )