Metamath Proof Explorer

Theorem 2ndresdju

Description: The 2nd function restricted to a disjoint union is injective. (Contributed by Thierry Arnoux, 23-Jun-2024)

Ref Expression
Hypotheses 2ndresdju.u 
|- U = U_ x e. X ( { x } X. C )
2ndresdju.a 
|- ( ph -> A e. V )
2ndresdju.x 
|- ( ph -> X e. W )
2ndresdju.1 
|- ( ph -> Disj_ x e. X C )
2ndresdju.2 
|- ( ph -> U_ x e. X C = A )
Assertion 2ndresdju 
|- ( ph -> ( 2nd |` U ) : U -1-1-> A )

Proof

Step Hyp Ref Expression
1 2ndresdju.u 
 |-  U = U_ x e. X ( { x } X. C )
2 2ndresdju.a 
 |-  ( ph -> A e. V )
3 2ndresdju.x 
 |-  ( ph -> X e. W )
4 2ndresdju.1 
 |-  ( ph -> Disj_ x e. X C )
5 2ndresdju.2 
 |-  ( ph -> U_ x e. X C = A )
6 fo2nd 
 |-  2nd : _V -onto-> _V
7 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
8 6 7 mp1i 
 |-  ( ph -> 2nd Fn _V )
9 ssv 
 |-  U C_ _V
10 9 a1i 
 |-  ( ph -> U C_ _V )
11 8 10 fnssresd 
 |-  ( ph -> ( 2nd |` U ) Fn U )
12 simpr 
 |-  ( ( ph /\ u e. U ) -> u e. U )
13 12 fvresd 
 |-  ( ( ph /\ u e. U ) -> ( ( 2nd |` U ) ` u ) = ( 2nd ` u ) )
14 djussxp2 
 |-  U_ x e. X ( { x } X. C ) C_ ( X X. U_ x e. X C )
15 5 xpeq2d 
 |-  ( ph -> ( X X. U_ x e. X C ) = ( X X. A ) )
16 14 15 sseqtrid 
 |-  ( ph -> U_ x e. X ( { x } X. C ) C_ ( X X. A ) )
17 1 16 eqsstrid 
 |-  ( ph -> U C_ ( X X. A ) )
18 17 sselda 
 |-  ( ( ph /\ u e. U ) -> u e. ( X X. A ) )
19 xp2nd 
 |-  ( u e. ( X X. A ) -> ( 2nd ` u ) e. A )
20 18 19 syl 
 |-  ( ( ph /\ u e. U ) -> ( 2nd ` u ) e. A )
21 13 20 eqeltrd 
 |-  ( ( ph /\ u e. U ) -> ( ( 2nd |` U ) ` u ) e. A )
22 21 ralrimiva 
 |-  ( ph -> A. u e. U ( ( 2nd |` U ) ` u ) e. A )
23 ffnfv 
 |-  ( ( 2nd |` U ) : U --> A <-> ( ( 2nd |` U ) Fn U /\ A. u e. U ( ( 2nd |` U ) ` u ) e. A ) )
24 11 22 23 sylanbrc 
 |-  ( ph -> ( 2nd |` U ) : U --> A )
25 nfv 
 |-  F/ x ph
26 nfiu1 
 |-  F/_ x U_ x e. X ( { x } X. C )
27 1 26 nfcxfr 
 |-  F/_ x U
28 27 nfcri 
 |-  F/ x u e. U
29 25 28 nfan 
 |-  F/ x ( ph /\ u e. U )
30 27 nfcri 
 |-  F/ x v e. U
31 29 30 nfan 
 |-  F/ x ( ( ph /\ u e. U ) /\ v e. U )
32 nfcv 
 |-  F/_ x 2nd
33 32 27 nfres 
 |-  F/_ x ( 2nd |` U )
34 nfcv 
 |-  F/_ x u
35 33 34 nffv 
 |-  F/_ x ( ( 2nd |` U ) ` u )
36 nfcv 
 |-  F/_ x v
37 33 36 nffv 
 |-  F/_ x ( ( 2nd |` U ) ` v )
38 35 37 nfeq 
 |-  F/ x ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v )
39 31 38 nfan 
 |-  F/ x ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) )
40 nfv 
 |-  F/ x u = v
41 1 eleq2i 
 |-  ( u e. U <-> u e. U_ x e. X ( { x } X. C ) )
42 eliunxp 
 |-  ( u e. U_ x e. X ( { x } X. C ) <-> E. x E. c ( u = <. x , c >. /\ ( x e. X /\ c e. C ) ) )
43 41 42 sylbb 
 |-  ( u e. U -> E. x E. c ( u = <. x , c >. /\ ( x e. X /\ c e. C ) ) )
44 43 ad3antlr 
 |-  ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) -> E. x E. c ( u = <. x , c >. /\ ( x e. X /\ c e. C ) ) )
45 1 eleq2i 
 |-  ( v e. U <-> v e. U_ x e. X ( { x } X. C ) )
46 eliunxp 
 |-  ( v e. U_ x e. X ( { x } X. C ) <-> E. x E. d ( v = <. x , d >. /\ ( x e. X /\ d e. C ) ) )
47 45 46 bitri 
 |-  ( v e. U <-> E. x E. d ( v = <. x , d >. /\ ( x e. X /\ d e. C ) ) )
48 nfv 
 |-  F/ y E. d ( v = <. x , d >. /\ ( x e. X /\ d e. C ) )
49 nfv 
 |-  F/ x v = <. y , d >.
50 nfv 
 |-  F/ x y e. X
51 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
52 51 nfcri 
 |-  F/ x d e. [_ y / x ]_ C
53 50 52 nfan 
 |-  F/ x ( y e. X /\ d e. [_ y / x ]_ C )
54 49 53 nfan 
 |-  F/ x ( v = <. y , d >. /\ ( y e. X /\ d e. [_ y / x ]_ C ) )
55 54 nfex 
 |-  F/ x E. d ( v = <. y , d >. /\ ( y e. X /\ d e. [_ y / x ]_ C ) )
56 opeq1 
 |-  ( x = y -> <. x , d >. = <. y , d >. )
57 56 eqeq2d 
 |-  ( x = y -> ( v = <. x , d >. <-> v = <. y , d >. ) )
58 eleq1w 
 |-  ( x = y -> ( x e. X <-> y e. X ) )
59 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
60 59 eleq2d 
 |-  ( x = y -> ( d e. C <-> d e. [_ y / x ]_ C ) )
61 58 60 anbi12d 
 |-  ( x = y -> ( ( x e. X /\ d e. C ) <-> ( y e. X /\ d e. [_ y / x ]_ C ) ) )
62 57 61 anbi12d 
 |-  ( x = y -> ( ( v = <. x , d >. /\ ( x e. X /\ d e. C ) ) <-> ( v = <. y , d >. /\ ( y e. X /\ d e. [_ y / x ]_ C ) ) ) )
63 62 exbidv 
 |-  ( x = y -> ( E. d ( v = <. x , d >. /\ ( x e. X /\ d e. C ) ) <-> E. d ( v = <. y , d >. /\ ( y e. X /\ d e. [_ y / x ]_ C ) ) ) )
64 48 55 63 cbvexv1 
 |-  ( E. x E. d ( v = <. x , d >. /\ ( x e. X /\ d e. C ) ) <-> E. y E. d ( v = <. y , d >. /\ ( y e. X /\ d e. [_ y / x ]_ C ) ) )
65 47 64 sylbb 
 |-  ( v e. U -> E. y E. d ( v = <. y , d >. /\ ( y e. X /\ d e. [_ y / x ]_ C ) ) )
66 65 ad5antlr 
 |-  ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) -> E. y E. d ( v = <. y , d >. /\ ( y e. X /\ d e. [_ y / x ]_ C ) ) )
67 4 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> Disj_ x e. X C )
68 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> x e. X )
69 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> y e. X )
70 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> c e. C )
71 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) )
72 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> u e. U )
73 72 fvresd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> ( ( 2nd |` U ) ` u ) = ( 2nd ` u ) )
74 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> u = <. x , c >. )
75 74 fveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> ( 2nd ` u ) = ( 2nd ` <. x , c >. ) )
76 vex 
 |-  x e. _V
77 vex 
 |-  c e. _V
78 76 77 op2nd 
 |-  ( 2nd ` <. x , c >. ) = c
79 75 78 eqtrdi 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> ( 2nd ` u ) = c )
80 73 79 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> ( ( 2nd |` U ) ` u ) = c )
81 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> v e. U )
82 81 fvresd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> ( ( 2nd |` U ) ` v ) = ( 2nd ` v ) )
83 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> v = <. y , d >. )
84 83 fveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> ( 2nd ` v ) = ( 2nd ` <. y , d >. ) )
85 vex 
 |-  y e. _V
86 vex 
 |-  d e. _V
87 85 86 op2nd 
 |-  ( 2nd ` <. y , d >. ) = d
88 84 87 eqtrdi 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> ( 2nd ` v ) = d )
89 82 88 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> ( ( 2nd |` U ) ` v ) = d )
90 71 80 89 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> c = d )
91 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> d e. [_ y / x ]_ C )
92 90 91 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> c e. [_ y / x ]_ C )
93 51 59 disjif 
 |-  ( ( Disj_ x e. X C /\ ( x e. X /\ y e. X ) /\ ( c e. C /\ c e. [_ y / x ]_ C ) ) -> x = y )
94 67 68 69 70 92 93 syl122anc 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> x = y )
95 94 90 opeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> <. x , c >. = <. y , d >. )
96 95 74 83 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ y e. X ) /\ d e. [_ y / x ]_ C ) -> u = v )
97 96 anasss 
 |-  ( ( ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) /\ v = <. y , d >. ) /\ ( y e. X /\ d e. [_ y / x ]_ C ) ) -> u = v )
98 97 expl 
 |-  ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) -> ( ( v = <. y , d >. /\ ( y e. X /\ d e. [_ y / x ]_ C ) ) -> u = v ) )
99 98 exlimdvv 
 |-  ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) -> ( E. y E. d ( v = <. y , d >. /\ ( y e. X /\ d e. [_ y / x ]_ C ) ) -> u = v ) )
100 66 99 mpd 
 |-  ( ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ x e. X ) /\ c e. C ) -> u = v )
101 100 anasss 
 |-  ( ( ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) /\ u = <. x , c >. ) /\ ( x e. X /\ c e. C ) ) -> u = v )
102 101 expl 
 |-  ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) -> ( ( u = <. x , c >. /\ ( x e. X /\ c e. C ) ) -> u = v ) )
103 102 exlimdv 
 |-  ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) -> ( E. c ( u = <. x , c >. /\ ( x e. X /\ c e. C ) ) -> u = v ) )
104 39 40 44 103 exlimimdd 
 |-  ( ( ( ( ph /\ u e. U ) /\ v e. U ) /\ ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) ) -> u = v )
105 104 ex 
 |-  ( ( ( ph /\ u e. U ) /\ v e. U ) -> ( ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) -> u = v ) )
106 105 anasss 
 |-  ( ( ph /\ ( u e. U /\ v e. U ) ) -> ( ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) -> u = v ) )
107 106 ralrimivva 
 |-  ( ph -> A. u e. U A. v e. U ( ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) -> u = v ) )
108 dff13 
 |-  ( ( 2nd |` U ) : U -1-1-> A <-> ( ( 2nd |` U ) : U --> A /\ A. u e. U A. v e. U ( ( ( 2nd |` U ) ` u ) = ( ( 2nd |` U ) ` v ) -> u = v ) ) )
109 24 107 108 sylanbrc 
 |-  ( ph -> ( 2nd |` U ) : U -1-1-> A )