Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  actfunsnf1o Structured version   Visualization version   GIF version

Theorem actfunsnf1o 33611
Description: The action 𝐹 of extending function from 𝐡 to 𝐢 with new values at point 𝐼 is a bijection. (Contributed by Thierry Arnoux, 9-Dec-2021.)
Hypotheses
Ref Expression
actfunsn.1 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ 𝐴 βŠ† (𝐢 ↑m 𝐡))
actfunsn.2 (πœ‘ β†’ 𝐢 ∈ V)
actfunsn.3 (πœ‘ β†’ 𝐼 ∈ 𝑉)
actfunsn.4 (πœ‘ β†’ Β¬ 𝐼 ∈ 𝐡)
actfunsn.5 𝐹 = (π‘₯ ∈ 𝐴 ↦ (π‘₯ βˆͺ {⟨𝐼, π‘˜βŸ©}))
Assertion
Ref Expression
actfunsnf1o ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ 𝐹:𝐴–1-1-ontoβ†’ran 𝐹)
Distinct variable groups:   π‘₯,𝐴   π‘˜,𝐼,π‘₯   πœ‘,π‘˜
Allowed substitution hints:   πœ‘(π‘₯)   𝐴(π‘˜)   𝐡(π‘₯,π‘˜)   𝐢(π‘₯,π‘˜)   𝐹(π‘₯,π‘˜)   𝑉(π‘₯,π‘˜)

Proof of Theorem actfunsnf1o
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 actfunsn.5 . . 3 𝐹 = (π‘₯ ∈ 𝐴 ↦ (π‘₯ βˆͺ {⟨𝐼, π‘˜βŸ©}))
2 uneq1 4156 . . . 4 (π‘₯ = 𝑧 β†’ (π‘₯ βˆͺ {⟨𝐼, π‘˜βŸ©}) = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
32cbvmptv 5261 . . 3 (π‘₯ ∈ 𝐴 ↦ (π‘₯ βˆͺ {⟨𝐼, π‘˜βŸ©})) = (𝑧 ∈ 𝐴 ↦ (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
41, 3eqtri 2760 . 2 𝐹 = (𝑧 ∈ 𝐴 ↦ (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
5 vex 3478 . . . 4 𝑧 ∈ V
6 snex 5431 . . . 4 {⟨𝐼, π‘˜βŸ©} ∈ V
75, 6unex 7732 . . 3 (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) ∈ V
87a1i 11 . 2 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) ∈ V)
9 vex 3478 . . . 4 𝑦 ∈ V
109resex 6029 . . 3 (𝑦 β†Ύ 𝐡) ∈ V
1110a1i 11 . 2 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) β†’ (𝑦 β†Ύ 𝐡) ∈ V)
12 rspe 3246 . . . . . . 7 ((𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ βˆƒπ‘§ ∈ 𝐴 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
134, 7elrnmpti 5959 . . . . . . 7 (𝑦 ∈ ran 𝐹 ↔ βˆƒπ‘§ ∈ 𝐴 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
1412, 13sylibr 233 . . . . . 6 ((𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑦 ∈ ran 𝐹)
1514adantll 712 . . . . 5 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑦 ∈ ran 𝐹)
16 simpr 485 . . . . . . 7 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
1716reseq1d 5980 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝑦 β†Ύ 𝐡) = ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡))
18 actfunsn.1 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ 𝐴 βŠ† (𝐢 ↑m 𝐡))
1918sselda 3982 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ 𝑧 ∈ (𝐢 ↑m 𝐡))
20 elmapfn 8858 . . . . . . . . 9 (𝑧 ∈ (𝐢 ↑m 𝐡) β†’ 𝑧 Fn 𝐡)
2119, 20syl 17 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ 𝑧 Fn 𝐡)
22 actfunsn.3 . . . . . . . . . 10 (πœ‘ β†’ 𝐼 ∈ 𝑉)
23 fnsng 6600 . . . . . . . . . 10 ((𝐼 ∈ 𝑉 ∧ π‘˜ ∈ 𝐢) β†’ {⟨𝐼, π‘˜βŸ©} Fn {𝐼})
2422, 23sylan 580 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ {⟨𝐼, π‘˜βŸ©} Fn {𝐼})
2524adantr 481 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ {⟨𝐼, π‘˜βŸ©} Fn {𝐼})
26 actfunsn.4 . . . . . . . . . . 11 (πœ‘ β†’ Β¬ 𝐼 ∈ 𝐡)
27 disjsn 4715 . . . . . . . . . . 11 ((𝐡 ∩ {𝐼}) = βˆ… ↔ Β¬ 𝐼 ∈ 𝐡)
2826, 27sylibr 233 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 ∩ {𝐼}) = βˆ…)
2928adantr 481 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ (𝐡 ∩ {𝐼}) = βˆ…)
3029adantr 481 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ (𝐡 ∩ {𝐼}) = βˆ…)
31 fnunres1 6661 . . . . . . . 8 ((𝑧 Fn 𝐡 ∧ {⟨𝐼, π‘˜βŸ©} Fn {𝐼} ∧ (𝐡 ∩ {𝐼}) = βˆ…) β†’ ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡) = 𝑧)
3221, 25, 30, 31syl3anc 1371 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡) = 𝑧)
3332adantr 481 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡) = 𝑧)
3417, 33eqtr2d 2773 . . . . 5 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑧 = (𝑦 β†Ύ 𝐡))
3515, 34jca 512 . . . 4 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 β†Ύ 𝐡)))
3635anasss 467 . . 3 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))) β†’ (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 β†Ύ 𝐡)))
37 simpr 485 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ 𝑧 = (𝑦 β†Ύ 𝐡))
38 simpr 485 . . . . . . . . . 10 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
3938reseq1d 5980 . . . . . . . . 9 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝑦 β†Ύ 𝐡) = ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡))
4018ad3antrrr 728 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝐴 βŠ† (𝐢 ↑m 𝐡))
41 simplr 767 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑧 ∈ 𝐴)
4240, 41sseldd 3983 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑧 ∈ (𝐢 ↑m 𝐡))
4342, 20syl 17 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑧 Fn 𝐡)
4422ad4antr 730 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝐼 ∈ 𝑉)
45 simp-4r 782 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ π‘˜ ∈ 𝐢)
4644, 45, 23syl2anc 584 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ {⟨𝐼, π‘˜βŸ©} Fn {𝐼})
4728ad4antr 730 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝐡 ∩ {𝐼}) = βˆ…)
4843, 46, 47, 31syl3anc 1371 . . . . . . . . . 10 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡) = 𝑧)
4948, 41eqeltrd 2833 . . . . . . . . 9 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡) ∈ 𝐴)
5039, 49eqeltrd 2833 . . . . . . . 8 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝑦 β†Ύ 𝐡) ∈ 𝐴)
51 simpr 485 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) β†’ 𝑦 ∈ ran 𝐹)
5251, 13sylib 217 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) β†’ βˆƒπ‘§ ∈ 𝐴 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
5350, 52r19.29a 3162 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) β†’ (𝑦 β†Ύ 𝐡) ∈ 𝐴)
5453adantr 481 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ (𝑦 β†Ύ 𝐡) ∈ 𝐴)
5537, 54eqeltrd 2833 . . . . 5 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ 𝑧 ∈ 𝐴)
5637uneq1d 4162 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) = ((𝑦 β†Ύ 𝐡) βˆͺ {⟨𝐼, π‘˜βŸ©}))
5739, 48eqtrd 2772 . . . . . . . . . 10 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝑦 β†Ύ 𝐡) = 𝑧)
5857uneq1d 4162 . . . . . . . . 9 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ ((𝑦 β†Ύ 𝐡) βˆͺ {⟨𝐼, π‘˜βŸ©}) = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
5958, 38eqtr4d 2775 . . . . . . . 8 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ ((𝑦 β†Ύ 𝐡) βˆͺ {⟨𝐼, π‘˜βŸ©}) = 𝑦)
6059, 52r19.29a 3162 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) β†’ ((𝑦 β†Ύ 𝐡) βˆͺ {⟨𝐼, π‘˜βŸ©}) = 𝑦)
6160adantr 481 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ ((𝑦 β†Ύ 𝐡) βˆͺ {⟨𝐼, π‘˜βŸ©}) = 𝑦)
6256, 61eqtr2d 2773 . . . . 5 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
6355, 62jca 512 . . . 4 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ (𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})))
6463anasss 467 . . 3 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 β†Ύ 𝐡))) β†’ (𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})))
6536, 64impbida 799 . 2 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ ((𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) ↔ (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 β†Ύ 𝐡))))
664, 8, 11, 65f1od 7657 1 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ 𝐹:𝐴–1-1-ontoβ†’ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆƒwrex 3070  Vcvv 3474   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628  βŸ¨cop 4634   ↦ cmpt 5231  ran crn 5677   β†Ύ cres 5678   Fn wfn 6538  β€“1-1-ontoβ†’wf1o 6542  (class class class)co 7408   ↑m cmap 8819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7974  df-2nd 7975  df-map 8821
This theorem is referenced by:  breprexplema  33637
  Copyright terms: Public domain W3C validator