Metamath Proof Explorer

Theorem disjf1o

Description: A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses disjf1o.xph 
|- F/ x ph
disjf1o.f 
|- F = ( x e. A |-> B )
disjf1o.b 
|- ( ( ph /\ x e. A ) -> B e. V )
disjf1o.dj 
|- ( ph -> Disj_ x e. A B )
disjf1o.d 
|- C = { x e. A | B =/= (/) }
disjf1o.e 
|- D = ( ran F \ { (/) } )
Assertion disjf1o 
|- ( ph -> ( F |` C ) : C -1-1-onto-> D )

Proof

Step Hyp Ref Expression
1 disjf1o.xph 
 |-  F/ x ph
2 disjf1o.f 
 |-  F = ( x e. A |-> B )
3 disjf1o.b 
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 disjf1o.dj 
 |-  ( ph -> Disj_ x e. A B )
5 disjf1o.d 
 |-  C = { x e. A | B =/= (/) }
6 disjf1o.e 
 |-  D = ( ran F \ { (/) } )
7 eqid 
 |-  ( x e. C |-> B ) = ( x e. C |-> B )
8 simpl 
 |-  ( ( ph /\ x e. C ) -> ph )
9 ssrab2 
 |-  { x e. A | B =/= (/) } C_ A
10 5 9 eqsstri 
 |-  C C_ A
11 id 
 |-  ( x e. C -> x e. C )
12 10 11 sselid 
 |-  ( x e. C -> x e. A )
13 12 adantl 
 |-  ( ( ph /\ x e. C ) -> x e. A )
14 8 13 3 syl2anc 
 |-  ( ( ph /\ x e. C ) -> B e. V )
15 11 5 eleqtrdi 
 |-  ( x e. C -> x e. { x e. A | B =/= (/) } )
16 rabid 
 |-  ( x e. { x e. A | B =/= (/) } <-> ( x e. A /\ B =/= (/) ) )
17 16 a1i 
 |-  ( x e. C -> ( x e. { x e. A | B =/= (/) } <-> ( x e. A /\ B =/= (/) ) ) )
18 15 17 mpbid 
 |-  ( x e. C -> ( x e. A /\ B =/= (/) ) )
19 18 simprd 
 |-  ( x e. C -> B =/= (/) )
20 19 adantl 
 |-  ( ( ph /\ x e. C ) -> B =/= (/) )
21 10 a1i 
 |-  ( ph -> C C_ A )
22 disjss1 
 |-  ( C C_ A -> ( Disj_ x e. A B -> Disj_ x e. C B ) )
23 21 4 22 sylc 
 |-  ( ph -> Disj_ x e. C B )
24 1 7 14 20 23 disjf1 
 |-  ( ph -> ( x e. C |-> B ) : C -1-1-> V )
25 f1f1orn 
 |-  ( ( x e. C |-> B ) : C -1-1-> V -> ( x e. C |-> B ) : C -1-1-onto-> ran ( x e. C |-> B ) )
26 24 25 syl 
 |-  ( ph -> ( x e. C |-> B ) : C -1-1-onto-> ran ( x e. C |-> B ) )
27 2 a1i 
 |-  ( ph -> F = ( x e. A |-> B ) )
28 27 reseq1d 
 |-  ( ph -> ( F |` C ) = ( ( x e. A |-> B ) |` C ) )
29 21 resmptd 
 |-  ( ph -> ( ( x e. A |-> B ) |` C ) = ( x e. C |-> B ) )
30 28 29 eqtrd 
 |-  ( ph -> ( F |` C ) = ( x e. C |-> B ) )
31 eqidd 
 |-  ( ph -> C = C )
32 simpl 
 |-  ( ( ph /\ y e. D ) -> ph )
33 id 
 |-  ( y e. D -> y e. D )
34 33 6 eleqtrdi 
 |-  ( y e. D -> y e. ( ran F \ { (/) } ) )
35 eldifsni 
 |-  ( y e. ( ran F \ { (/) } ) -> y =/= (/) )
36 34 35 syl 
 |-  ( y e. D -> y =/= (/) )
37 36 adantl 
 |-  ( ( ph /\ y e. D ) -> y =/= (/) )
38 eldifi 
 |-  ( y e. ( ran F \ { (/) } ) -> y e. ran F )
39 34 38 syl 
 |-  ( y e. D -> y e. ran F )
40 2 elrnmpt 
 |-  ( y e. ran F -> ( y e. ran F <-> E. x e. A y = B ) )
41 39 40 syl 
 |-  ( y e. D -> ( y e. ran F <-> E. x e. A y = B ) )
42 39 41 mpbid 
 |-  ( y e. D -> E. x e. A y = B )
43 42 adantl 
 |-  ( ( ph /\ y e. D ) -> E. x e. A y = B )
44 nfv 
 |-  F/ x y =/= (/)
45 1 44 nfan 
 |-  F/ x ( ph /\ y =/= (/) )
46 nfcv 
 |-  F/_ x y
47 nfmpt1 
 |-  F/_ x ( x e. C |-> B )
48 47 nfrn 
 |-  F/_ x ran ( x e. C |-> B )
49 46 48 nfel 
 |-  F/ x y e. ran ( x e. C |-> B )
50 simp3 
 |-  ( ( y =/= (/) /\ x e. A /\ y = B ) -> y = B )
51 simp2 
 |-  ( ( y =/= (/) /\ x e. A /\ y = B ) -> x e. A )
52 id 
 |-  ( y = B -> y = B )
53 52 eqcomd 
 |-  ( y = B -> B = y )
54 53 adantl 
 |-  ( ( y =/= (/) /\ y = B ) -> B = y )
55 simpl 
 |-  ( ( y =/= (/) /\ y = B ) -> y =/= (/) )
56 54 55 eqnetrd 
 |-  ( ( y =/= (/) /\ y = B ) -> B =/= (/) )
57 56 3adant2 
 |-  ( ( y =/= (/) /\ x e. A /\ y = B ) -> B =/= (/) )
58 51 57 jca 
 |-  ( ( y =/= (/) /\ x e. A /\ y = B ) -> ( x e. A /\ B =/= (/) ) )
59 58 16 sylibr 
 |-  ( ( y =/= (/) /\ x e. A /\ y = B ) -> x e. { x e. A | B =/= (/) } )
60 5 eqcomi 
 |-  { x e. A | B =/= (/) } = C
61 60 a1i 
 |-  ( ( y =/= (/) /\ x e. A /\ y = B ) -> { x e. A | B =/= (/) } = C )
62 59 61 eleqtrd 
 |-  ( ( y =/= (/) /\ x e. A /\ y = B ) -> x e. C )
63 eqvisset 
 |-  ( y = B -> B e. _V )
64 63 3ad2ant3 
 |-  ( ( y =/= (/) /\ x e. A /\ y = B ) -> B e. _V )
65 7 elrnmpt1 
 |-  ( ( x e. C /\ B e. _V ) -> B e. ran ( x e. C |-> B ) )
66 62 64 65 syl2anc 
 |-  ( ( y =/= (/) /\ x e. A /\ y = B ) -> B e. ran ( x e. C |-> B ) )
67 50 66 eqeltrd 
 |-  ( ( y =/= (/) /\ x e. A /\ y = B ) -> y e. ran ( x e. C |-> B ) )
68 67 3adant1l 
 |-  ( ( ( ph /\ y =/= (/) ) /\ x e. A /\ y = B ) -> y e. ran ( x e. C |-> B ) )
69 68 3exp 
 |-  ( ( ph /\ y =/= (/) ) -> ( x e. A -> ( y = B -> y e. ran ( x e. C |-> B ) ) ) )
70 45 49 69 rexlimd 
 |-  ( ( ph /\ y =/= (/) ) -> ( E. x e. A y = B -> y e. ran ( x e. C |-> B ) ) )
71 70 imp 
 |-  ( ( ( ph /\ y =/= (/) ) /\ E. x e. A y = B ) -> y e. ran ( x e. C |-> B ) )
72 32 37 43 71 syl21anc 
 |-  ( ( ph /\ y e. D ) -> y e. ran ( x e. C |-> B ) )
73 72 ralrimiva 
 |-  ( ph -> A. y e. D y e. ran ( x e. C |-> B ) )
74 dfss3 
 |-  ( D C_ ran ( x e. C |-> B ) <-> A. y e. D y e. ran ( x e. C |-> B ) )
75 73 74 sylibr 
 |-  ( ph -> D C_ ran ( x e. C |-> B ) )
76 simpl 
 |-  ( ( ph /\ y e. ran ( x e. C |-> B ) ) -> ph )
77 vex 
 |-  y e. _V
78 7 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( x e. C |-> B ) <-> E. x e. C y = B ) )
79 77 78 ax-mp 
 |-  ( y e. ran ( x e. C |-> B ) <-> E. x e. C y = B )
80 79 biimpi 
 |-  ( y e. ran ( x e. C |-> B ) -> E. x e. C y = B )
81 80 adantl 
 |-  ( ( ph /\ y e. ran ( x e. C |-> B ) ) -> E. x e. C y = B )
82 nfv 
 |-  F/ x y e. D
83 simpr 
 |-  ( ( x e. C /\ y = B ) -> y = B )
84 12 adantr 
 |-  ( ( x e. C /\ y = B ) -> x e. A )
85 83 63 syl 
 |-  ( ( x e. C /\ y = B ) -> B e. _V )
86 2 elrnmpt1 
 |-  ( ( x e. A /\ B e. _V ) -> B e. ran F )
87 84 85 86 syl2anc 
 |-  ( ( x e. C /\ y = B ) -> B e. ran F )
88 83 87 eqeltrd 
 |-  ( ( x e. C /\ y = B ) -> y e. ran F )
89 88 3adant1 
 |-  ( ( ph /\ x e. C /\ y = B ) -> y e. ran F )
90 19 adantr 
 |-  ( ( x e. C /\ y = B ) -> B =/= (/) )
91 83 90 eqnetrd 
 |-  ( ( x e. C /\ y = B ) -> y =/= (/) )
92 nelsn 
 |-  ( y =/= (/) -> -. y e. { (/) } )
93 91 92 syl 
 |-  ( ( x e. C /\ y = B ) -> -. y e. { (/) } )
94 93 3adant1 
 |-  ( ( ph /\ x e. C /\ y = B ) -> -. y e. { (/) } )
95 89 94 eldifd 
 |-  ( ( ph /\ x e. C /\ y = B ) -> y e. ( ran F \ { (/) } ) )
96 95 6 eleqtrrdi 
 |-  ( ( ph /\ x e. C /\ y = B ) -> y e. D )
97 96 3exp 
 |-  ( ph -> ( x e. C -> ( y = B -> y e. D ) ) )
98 1 82 97 rexlimd 
 |-  ( ph -> ( E. x e. C y = B -> y e. D ) )
99 98 imp 
 |-  ( ( ph /\ E. x e. C y = B ) -> y e. D )
100 76 81 99 syl2anc 
 |-  ( ( ph /\ y e. ran ( x e. C |-> B ) ) -> y e. D )
101 75 100 eqelssd 
 |-  ( ph -> D = ran ( x e. C |-> B ) )
102 30 31 101 f1oeq123d 
 |-  ( ph -> ( ( F |` C ) : C -1-1-onto-> D <-> ( x e. C |-> B ) : C -1-1-onto-> ran ( x e. C |-> B ) ) )
103 26 102 mpbird 
 |-  ( ph -> ( F |` C ) : C -1-1-onto-> D )