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 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐴 ⊆ ( 𝐶 ↑m 𝐵 ) )
actfunsn.2 ⊢ ( 𝜑 → 𝐶 ∈ V )
actfunsn.3 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
actfunsn.4 ⊢ ( 𝜑 → ¬ 𝐼 ∈ 𝐵 )
actfunsn.5 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
Assertion actfunsnf1o ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 actfunsn.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐴 ⊆ ( 𝐶 ↑m 𝐵 ) )
2 actfunsn.2 ⊢ ( 𝜑 → 𝐶 ∈ V )
3 actfunsn.3 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 actfunsn.4 ⊢ ( 𝜑 → ¬ 𝐼 ∈ 𝐵 )
5 actfunsn.5 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
6 uneq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
7 6 cbvmptv ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
8 5 7 eqtri ⊢ 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
9 vex ⊢ 𝑧 ∈ V
10 snex ⊢ { ⟨ 𝐼 , 𝑘 ⟩ } ∈ V
11 9 10 unex ⊢ ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ∈ V
12 11 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ∈ V )
13 vex ⊢ 𝑦 ∈ V
14 13 resex ⊢ ( 𝑦 ↾ 𝐵 ) ∈ V
15 14 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 ↾ 𝐵 ) ∈ V )
16 rspe ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
17 8 11 elrnmpti ⊢ ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
18 16 17 sylibr ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝑦 ∈ ran 𝐹 )
19 18 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝑦 ∈ ran 𝐹 )
20 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
21 20 reseq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( 𝑦 ↾ 𝐵 ) = ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ↾ 𝐵 ) )
22 1 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ( 𝐶 ↑m 𝐵 ) )
23 elmapfn ⊢ ( 𝑧 ∈ ( 𝐶 ↑m 𝐵 ) → 𝑧 Fn 𝐵 )
24 22 23 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 Fn 𝐵 )
25 fnsng ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑘 ∈ 𝐶 ) → { ⟨ 𝐼 , 𝑘 ⟩ } Fn { 𝐼 } )
26 3 25 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → { ⟨ 𝐼 , 𝑘 ⟩ } Fn { 𝐼 } )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → { ⟨ 𝐼 , 𝑘 ⟩ } Fn { 𝐼 } )
28 disjsn ⊢ ( ( 𝐵 ∩ { 𝐼 } ) = ∅ ↔ ¬ 𝐼 ∈ 𝐵 )
29 4 28 sylibr ⊢ ( 𝜑 → ( 𝐵 ∩ { 𝐼 } ) = ∅ )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( 𝐵 ∩ { 𝐼 } ) = ∅ )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐵 ∩ { 𝐼 } ) = ∅ )
32 fnunres1 ⊢ ( ( 𝑧 Fn 𝐵 ∧ { ⟨ 𝐼 , 𝑘 ⟩ } Fn { 𝐼 } ∧ ( 𝐵 ∩ { 𝐼 } ) = ∅ ) → ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ↾ 𝐵 ) = 𝑧 )
33 24 27 31 32 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ↾ 𝐵 ) = 𝑧 )
34 33 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ↾ 𝐵 ) = 𝑧 )
35 21 34 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝑧 = ( 𝑦 ↾ 𝐵 ) )
36 19 35 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( 𝑦 ∈ ran 𝐹 ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) )
37 36 anasss ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) ) → ( 𝑦 ∈ ran 𝐹 ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) )
38 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) → 𝑧 = ( 𝑦 ↾ 𝐵 ) )
39 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
40 39 reseq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( 𝑦 ↾ 𝐵 ) = ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ↾ 𝐵 ) )
41 1 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝐴 ⊆ ( 𝐶 ↑m 𝐵 ) )
42 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝑧 ∈ 𝐴 )
43 41 42 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝑧 ∈ ( 𝐶 ↑m 𝐵 ) )
44 43 23 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝑧 Fn 𝐵 )
45 3 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝐼 ∈ 𝑉 )
46 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → 𝑘 ∈ 𝐶 )
47 45 46 25 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → { ⟨ 𝐼 , 𝑘 ⟩ } Fn { 𝐼 } )
48 29 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( 𝐵 ∩ { 𝐼 } ) = ∅ )
49 44 47 48 32 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ↾ 𝐵 ) = 𝑧 )
50 49 42 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ↾ 𝐵 ) ∈ 𝐴 )
51 40 50 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( 𝑦 ↾ 𝐵 ) ∈ 𝐴 )
52 17 bilani ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
53 51 52 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( 𝑦 ↾ 𝐵 ) ∈ 𝐴 )
54 53 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) → ( 𝑦 ↾ 𝐵 ) ∈ 𝐴 )
55 38 54 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) → 𝑧 ∈ 𝐴 )
56 38 uneq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) → ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) = ( ( 𝑦 ↾ 𝐵 ) ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
57 40 49 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( 𝑦 ↾ 𝐵 ) = 𝑧 )
58 57 uneq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( ( 𝑦 ↾ 𝐵 ) ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
59 58 39 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) → ( ( 𝑦 ↾ 𝐵 ) ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) = 𝑦 )
60 59 52 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) → ( ( 𝑦 ↾ 𝐵 ) ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) = 𝑦 )
61 60 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) → ( ( 𝑦 ↾ 𝐵 ) ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) = 𝑦 )
62 56 61 eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) → 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) )
63 55 62 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ 𝑦 ∈ ran 𝐹 ) ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) → ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) )
64 63 anasss ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) ∧ ( 𝑦 ∈ ran 𝐹 ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) ) → ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) )
65 37 64 impbida ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 = ( 𝑧 ∪ { ⟨ 𝐼 , 𝑘 ⟩ } ) ) ↔ ( 𝑦 ∈ ran 𝐹 ∧ 𝑧 = ( 𝑦 ↾ 𝐵 ) ) ) )
66 8 12 15 65 f1od ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )