Metamath Proof Explorer

Theorem disjf1

Description: A 1 to 1 mapping built from disjoint, nonempty sets. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses disjf1.xph 
|- F/ x ph
disjf1.f 
|- F = ( x e. A |-> B )
disjf1.b 
|- ( ( ph /\ x e. A ) -> B e. V )
disjf1.n0 
|- ( ( ph /\ x e. A ) -> B =/= (/) )
disjf1.dj 
|- ( ph -> Disj_ x e. A B )
Assertion disjf1 
|- ( ph -> F : A -1-1-> V )

Proof

Step Hyp Ref Expression
1 disjf1.xph 
 |-  F/ x ph
2 disjf1.f 
 |-  F = ( x e. A |-> B )
3 disjf1.b 
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 disjf1.n0 
 |-  ( ( ph /\ x e. A ) -> B =/= (/) )
5 disjf1.dj 
 |-  ( ph -> Disj_ x e. A B )
6 nfv 
 |-  F/ x y e. A
7 1 6 nfan 
 |-  F/ x ( ph /\ y e. A )
8 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
9 nfcv 
 |-  F/_ x V
10 8 9 nfel 
 |-  F/ x [_ y / x ]_ B e. V
11 7 10 nfim 
 |-  F/ x ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. V )
12 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
13 12 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. A ) <-> ( ph /\ y e. A ) ) )
14 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
15 14 eleq1d 
 |-  ( x = y -> ( B e. V <-> [_ y / x ]_ B e. V ) )
16 13 15 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> B e. V ) <-> ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. V ) ) )
17 11 16 3 chvarfv 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. V )
18 17 ralrimiva 
 |-  ( ph -> A. y e. A [_ y / x ]_ B e. V )
19 inidm 
 |-  ( [_ y / x ]_ B i^i [_ y / x ]_ B ) = [_ y / x ]_ B
20 19 eqcomi 
 |-  [_ y / x ]_ B = ( [_ y / x ]_ B i^i [_ y / x ]_ B )
21 20 a1i 
 |-  ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> [_ y / x ]_ B = ( [_ y / x ]_ B i^i [_ y / x ]_ B ) )
22 ineq2 
 |-  ( [_ y / x ]_ B = [_ z / x ]_ B -> ( [_ y / x ]_ B i^i [_ y / x ]_ B ) = ( [_ y / x ]_ B i^i [_ z / x ]_ B ) )
23 22 ad2antlr 
 |-  ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> ( [_ y / x ]_ B i^i [_ y / x ]_ B ) = ( [_ y / x ]_ B i^i [_ z / x ]_ B ) )
24 nfcv 
 |-  F/_ w B
25 nfcsb1v 
 |-  F/_ x [_ w / x ]_ B
26 csbeq1a 
 |-  ( x = w -> B = [_ w / x ]_ B )
27 24 25 26 cbvdisj 
 |-  ( Disj_ x e. A B <-> Disj_ w e. A [_ w / x ]_ B )
28 5 27 sylib 
 |-  ( ph -> Disj_ w e. A [_ w / x ]_ B )
29 28 ad3antrrr 
 |-  ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> Disj_ w e. A [_ w / x ]_ B )
30 simpllr 
 |-  ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> ( y e. A /\ z e. A ) )
31 neqne 
 |-  ( -. y = z -> y =/= z )
32 31 adantl 
 |-  ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> y =/= z )
33 csbeq1 
 |-  ( w = y -> [_ w / x ]_ B = [_ y / x ]_ B )
34 csbeq1 
 |-  ( w = z -> [_ w / x ]_ B = [_ z / x ]_ B )
35 33 34 disji2 
 |-  ( ( Disj_ w e. A [_ w / x ]_ B /\ ( y e. A /\ z e. A ) /\ y =/= z ) -> ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) )
36 29 30 32 35 syl3anc 
 |-  ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) )
37 21 23 36 3eqtrd 
 |-  ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> [_ y / x ]_ B = (/) )
38 nfcv 
 |-  F/_ x (/)
39 8 38 nfne 
 |-  F/ x [_ y / x ]_ B =/= (/)
40 7 39 nfim 
 |-  F/ x ( ( ph /\ y e. A ) -> [_ y / x ]_ B =/= (/) )
41 14 neeq1d 
 |-  ( x = y -> ( B =/= (/) <-> [_ y / x ]_ B =/= (/) ) )
42 13 41 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> B =/= (/) ) <-> ( ( ph /\ y e. A ) -> [_ y / x ]_ B =/= (/) ) ) )
43 40 42 4 chvarfv 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B =/= (/) )
44 43 adantrr 
 |-  ( ( ph /\ ( y e. A /\ z e. A ) ) -> [_ y / x ]_ B =/= (/) )
45 44 ad2antrr 
 |-  ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> [_ y / x ]_ B =/= (/) )
46 45 neneqd 
 |-  ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> -. [_ y / x ]_ B = (/) )
47 37 46 condan 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) -> y = z )
48 47 ex 
 |-  ( ( ph /\ ( y e. A /\ z e. A ) ) -> ( [_ y / x ]_ B = [_ z / x ]_ B -> y = z ) )
49 48 ralrimivva 
 |-  ( ph -> A. y e. A A. z e. A ( [_ y / x ]_ B = [_ z / x ]_ B -> y = z ) )
50 18 49 jca 
 |-  ( ph -> ( A. y e. A [_ y / x ]_ B e. V /\ A. y e. A A. z e. A ( [_ y / x ]_ B = [_ z / x ]_ B -> y = z ) ) )
51 nfcv 
 |-  F/_ y B
52 51 8 14 cbvmpt 
 |-  ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
53 2 52 eqtri 
 |-  F = ( y e. A |-> [_ y / x ]_ B )
54 csbeq1 
 |-  ( y = z -> [_ y / x ]_ B = [_ z / x ]_ B )
55 53 54 f1mpt 
 |-  ( F : A -1-1-> V <-> ( A. y e. A [_ y / x ]_ B e. V /\ A. y e. A A. z e. A ( [_ y / x ]_ B = [_ z / x ]_ B -> y = z ) ) )
56 50 55 sylibr 
 |-  ( ph -> F : A -1-1-> V )