Metamath Proof Explorer

Theorem actfunsnf1o

Description: The action F of extending function from B to C with new values at point I is a bijection. (Contributed by Thierry Arnoux, 9-Dec-2021)

Ref Expression
Hypotheses actfunsn.1 
|- ( ( ph /\ k e. C ) -> A C_ ( C ^m B ) )
actfunsn.2 
|- ( ph -> C e. _V )
actfunsn.3 
|- ( ph -> I e. V )
actfunsn.4 
|- ( ph -> -. I e. B )
actfunsn.5 
|- F = ( x e. A |-> ( x u. { <. I , k >. } ) )
Assertion actfunsnf1o 
|- ( ( ph /\ k e. C ) -> F : A -1-1-onto-> ran F )

Proof

Step Hyp Ref Expression
1 actfunsn.1 
 |-  ( ( ph /\ k e. C ) -> A C_ ( C ^m B ) )
2 actfunsn.2 
 |-  ( ph -> C e. _V )
3 actfunsn.3 
 |-  ( ph -> I e. V )
4 actfunsn.4 
 |-  ( ph -> -. I e. B )
5 actfunsn.5 
 |-  F = ( x e. A |-> ( x u. { <. I , k >. } ) )
6 uneq1 
 |-  ( x = z -> ( x u. { <. I , k >. } ) = ( z u. { <. I , k >. } ) )
7 6 cbvmptv 
 |-  ( x e. A |-> ( x u. { <. I , k >. } ) ) = ( z e. A |-> ( z u. { <. I , k >. } ) )
8 5 7 eqtri 
 |-  F = ( z e. A |-> ( z u. { <. I , k >. } ) )
9 vex 
 |-  z e. _V
10 snex 
 |-  { <. I , k >. } e. _V
11 9 10 unex 
 |-  ( z u. { <. I , k >. } ) e. _V
12 11 a1i 
 |-  ( ( ( ph /\ k e. C ) /\ z e. A ) -> ( z u. { <. I , k >. } ) e. _V )
13 vex 
 |-  y e. _V
14 13 resex 
 |-  ( y |` B ) e. _V
15 14 a1i 
 |-  ( ( ( ph /\ k e. C ) /\ y e. ran F ) -> ( y |` B ) e. _V )
16 rspe 
 |-  ( ( z e. A /\ y = ( z u. { <. I , k >. } ) ) -> E. z e. A y = ( z u. { <. I , k >. } ) )
17 8 11 elrnmpti 
 |-  ( y e. ran F <-> E. z e. A y = ( z u. { <. I , k >. } ) )
18 16 17 sylibr 
 |-  ( ( z e. A /\ y = ( z u. { <. I , k >. } ) ) -> y e. ran F )
19 18 adantll 
 |-  ( ( ( ( ph /\ k e. C ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> y e. ran F )
20 simpr 
 |-  ( ( ( ( ph /\ k e. C ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> y = ( z u. { <. I , k >. } ) )
21 20 reseq1d 
 |-  ( ( ( ( ph /\ k e. C ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( y |` B ) = ( ( z u. { <. I , k >. } ) |` B ) )
22 1 sselda 
 |-  ( ( ( ph /\ k e. C ) /\ z e. A ) -> z e. ( C ^m B ) )
23 elmapfn 
 |-  ( z e. ( C ^m B ) -> z Fn B )
24 22 23 syl 
 |-  ( ( ( ph /\ k e. C ) /\ z e. A ) -> z Fn B )
25 fnsng 
 |-  ( ( I e. V /\ k e. C ) -> { <. I , k >. } Fn { I } )
26 3 25 sylan 
 |-  ( ( ph /\ k e. C ) -> { <. I , k >. } Fn { I } )
27 26 adantr 
 |-  ( ( ( ph /\ k e. C ) /\ z e. A ) -> { <. I , k >. } Fn { I } )
28 disjsn 
 |-  ( ( B i^i { I } ) = (/) <-> -. I e. B )
29 4 28 sylibr 
 |-  ( ph -> ( B i^i { I } ) = (/) )
30 29 adantr 
 |-  ( ( ph /\ k e. C ) -> ( B i^i { I } ) = (/) )
31 30 adantr 
 |-  ( ( ( ph /\ k e. C ) /\ z e. A ) -> ( B i^i { I } ) = (/) )
32 fnunres1 
 |-  ( ( z Fn B /\ { <. I , k >. } Fn { I } /\ ( B i^i { I } ) = (/) ) -> ( ( z u. { <. I , k >. } ) |` B ) = z )
33 24 27 31 32 syl3anc 
 |-  ( ( ( ph /\ k e. C ) /\ z e. A ) -> ( ( z u. { <. I , k >. } ) |` B ) = z )
34 33 adantr 
 |-  ( ( ( ( ph /\ k e. C ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( ( z u. { <. I , k >. } ) |` B ) = z )
35 21 34 eqtr2d 
 |-  ( ( ( ( ph /\ k e. C ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> z = ( y |` B ) )
36 19 35 jca 
 |-  ( ( ( ( ph /\ k e. C ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( y e. ran F /\ z = ( y |` B ) ) )
37 36 anasss 
 |-  ( ( ( ph /\ k e. C ) /\ ( z e. A /\ y = ( z u. { <. I , k >. } ) ) ) -> ( y e. ran F /\ z = ( y |` B ) ) )
38 simpr 
 |-  ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z = ( y |` B ) ) -> z = ( y |` B ) )
39 simpr 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> y = ( z u. { <. I , k >. } ) )
40 39 reseq1d 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( y |` B ) = ( ( z u. { <. I , k >. } ) |` B ) )
41 1 ad3antrrr 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> A C_ ( C ^m B ) )
42 simplr 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> z e. A )
43 41 42 sseldd 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> z e. ( C ^m B ) )
44 43 23 syl 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> z Fn B )
45 3 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> I e. V )
46 simp-4r 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> k e. C )
47 45 46 25 syl2anc 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> { <. I , k >. } Fn { I } )
48 29 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( B i^i { I } ) = (/) )
49 44 47 48 32 syl3anc 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( ( z u. { <. I , k >. } ) |` B ) = z )
50 49 42 eqeltrd 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( ( z u. { <. I , k >. } ) |` B ) e. A )
51 40 50 eqeltrd 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( y |` B ) e. A )
52 simpr 
 |-  ( ( ( ph /\ k e. C ) /\ y e. ran F ) -> y e. ran F )
53 52 17 sylib 
 |-  ( ( ( ph /\ k e. C ) /\ y e. ran F ) -> E. z e. A y = ( z u. { <. I , k >. } ) )
54 51 53 r19.29a 
 |-  ( ( ( ph /\ k e. C ) /\ y e. ran F ) -> ( y |` B ) e. A )
55 54 adantr 
 |-  ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z = ( y |` B ) ) -> ( y |` B ) e. A )
56 38 55 eqeltrd 
 |-  ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z = ( y |` B ) ) -> z e. A )
57 38 uneq1d 
 |-  ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z = ( y |` B ) ) -> ( z u. { <. I , k >. } ) = ( ( y |` B ) u. { <. I , k >. } ) )
58 40 49 eqtrd 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( y |` B ) = z )
59 58 uneq1d 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( ( y |` B ) u. { <. I , k >. } ) = ( z u. { <. I , k >. } ) )
60 59 39 eqtr4d 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z e. A ) /\ y = ( z u. { <. I , k >. } ) ) -> ( ( y |` B ) u. { <. I , k >. } ) = y )
61 60 53 r19.29a 
 |-  ( ( ( ph /\ k e. C ) /\ y e. ran F ) -> ( ( y |` B ) u. { <. I , k >. } ) = y )
62 61 adantr 
 |-  ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z = ( y |` B ) ) -> ( ( y |` B ) u. { <. I , k >. } ) = y )
63 57 62 eqtr2d 
 |-  ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z = ( y |` B ) ) -> y = ( z u. { <. I , k >. } ) )
64 56 63 jca 
 |-  ( ( ( ( ph /\ k e. C ) /\ y e. ran F ) /\ z = ( y |` B ) ) -> ( z e. A /\ y = ( z u. { <. I , k >. } ) ) )
65 64 anasss 
 |-  ( ( ( ph /\ k e. C ) /\ ( y e. ran F /\ z = ( y |` B ) ) ) -> ( z e. A /\ y = ( z u. { <. I , k >. } ) ) )
66 37 65 impbida 
 |-  ( ( ph /\ k e. C ) -> ( ( z e. A /\ y = ( z u. { <. I , k >. } ) ) <-> ( y e. ran F /\ z = ( y |` B ) ) ) )
67 8 12 15 66 f1od 
 |-  ( ( ph /\ k e. C ) -> F : A -1-1-onto-> ran F )