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 )