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 33281
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 4120 . . . 4 (π‘₯ = 𝑧 β†’ (π‘₯ βˆͺ {⟨𝐼, π‘˜βŸ©}) = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
32cbvmptv 5222 . . 3 (π‘₯ ∈ 𝐴 ↦ (π‘₯ βˆͺ {⟨𝐼, π‘˜βŸ©})) = (𝑧 ∈ 𝐴 ↦ (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
41, 3eqtri 2761 . 2 𝐹 = (𝑧 ∈ 𝐴 ↦ (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
5 vex 3451 . . . 4 𝑧 ∈ V
6 snex 5392 . . . 4 {⟨𝐼, π‘˜βŸ©} ∈ V
75, 6unex 7684 . . 3 (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) ∈ V
87a1i 11 . 2 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) ∈ V)
9 vex 3451 . . . 4 𝑦 ∈ V
109resex 5989 . . 3 (𝑦 β†Ύ 𝐡) ∈ V
1110a1i 11 . 2 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) β†’ (𝑦 β†Ύ 𝐡) ∈ V)
12 rspe 3231 . . . . . . 7 ((𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ βˆƒπ‘§ ∈ 𝐴 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
134, 7elrnmpti 5919 . . . . . . 7 (𝑦 ∈ ran 𝐹 ↔ βˆƒπ‘§ ∈ 𝐴 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
1412, 13sylibr 233 . . . . . 6 ((𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑦 ∈ ran 𝐹)
1514adantll 713 . . . . 5 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑦 ∈ ran 𝐹)
16 simpr 486 . . . . . . 7 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
1716reseq1d 5940 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝑦 β†Ύ 𝐡) = ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡))
18 actfunsn.1 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ 𝐴 βŠ† (𝐢 ↑m 𝐡))
1918sselda 3948 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ 𝑧 ∈ (𝐢 ↑m 𝐡))
20 elmapfn 8809 . . . . . . . . 9 (𝑧 ∈ (𝐢 ↑m 𝐡) β†’ 𝑧 Fn 𝐡)
2119, 20syl 17 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ 𝑧 Fn 𝐡)
22 actfunsn.3 . . . . . . . . . 10 (πœ‘ β†’ 𝐼 ∈ 𝑉)
23 fnsng 6557 . . . . . . . . . 10 ((𝐼 ∈ 𝑉 ∧ π‘˜ ∈ 𝐢) β†’ {⟨𝐼, π‘˜βŸ©} Fn {𝐼})
2422, 23sylan 581 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ {⟨𝐼, π‘˜βŸ©} Fn {𝐼})
2524adantr 482 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ {⟨𝐼, π‘˜βŸ©} Fn {𝐼})
26 actfunsn.4 . . . . . . . . . . 11 (πœ‘ β†’ Β¬ 𝐼 ∈ 𝐡)
27 disjsn 4676 . . . . . . . . . . 11 ((𝐡 ∩ {𝐼}) = βˆ… ↔ Β¬ 𝐼 ∈ 𝐡)
2826, 27sylibr 233 . . . . . . . . . 10 (πœ‘ β†’ (𝐡 ∩ {𝐼}) = βˆ…)
2928adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ (𝐡 ∩ {𝐼}) = βˆ…)
3029adantr 482 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ (𝐡 ∩ {𝐼}) = βˆ…)
31 fnunres1 31577 . . . . . . . 8 ((𝑧 Fn 𝐡 ∧ {⟨𝐼, π‘˜βŸ©} Fn {𝐼} ∧ (𝐡 ∩ {𝐼}) = βˆ…) β†’ ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡) = 𝑧)
3221, 25, 30, 31syl3anc 1372 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) β†’ ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡) = 𝑧)
3332adantr 482 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡) = 𝑧)
3417, 33eqtr2d 2774 . . . . 5 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑧 = (𝑦 β†Ύ 𝐡))
3515, 34jca 513 . . . 4 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 β†Ύ 𝐡)))
3635anasss 468 . . 3 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))) β†’ (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 β†Ύ 𝐡)))
37 simpr 486 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ 𝑧 = (𝑦 β†Ύ 𝐡))
38 simpr 486 . . . . . . . . . 10 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
3938reseq1d 5940 . . . . . . . . 9 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝑦 β†Ύ 𝐡) = ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡))
4018ad3antrrr 729 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝐴 βŠ† (𝐢 ↑m 𝐡))
41 simplr 768 . . . . . . . . . . . . 13 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑧 ∈ 𝐴)
4240, 41sseldd 3949 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑧 ∈ (𝐢 ↑m 𝐡))
4342, 20syl 17 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝑧 Fn 𝐡)
4422ad4antr 731 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ 𝐼 ∈ 𝑉)
45 simp-4r 783 . . . . . . . . . . . 12 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ π‘˜ ∈ 𝐢)
4644, 45, 23syl2anc 585 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ {⟨𝐼, π‘˜βŸ©} Fn {𝐼})
4728ad4antr 731 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝐡 ∩ {𝐼}) = βˆ…)
4843, 46, 47, 31syl3anc 1372 . . . . . . . . . 10 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡) = 𝑧)
4948, 41eqeltrd 2834 . . . . . . . . 9 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ ((𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) β†Ύ 𝐡) ∈ 𝐴)
5039, 49eqeltrd 2834 . . . . . . . 8 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝑦 β†Ύ 𝐡) ∈ 𝐴)
51 simpr 486 . . . . . . . . 9 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) β†’ 𝑦 ∈ ran 𝐹)
5251, 13sylib 217 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) β†’ βˆƒπ‘§ ∈ 𝐴 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
5350, 52r19.29a 3156 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) β†’ (𝑦 β†Ύ 𝐡) ∈ 𝐴)
5453adantr 482 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ (𝑦 β†Ύ 𝐡) ∈ 𝐴)
5537, 54eqeltrd 2834 . . . . 5 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ 𝑧 ∈ 𝐴)
5637uneq1d 4126 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}) = ((𝑦 β†Ύ 𝐡) βˆͺ {⟨𝐼, π‘˜βŸ©}))
5739, 48eqtrd 2773 . . . . . . . . . 10 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ (𝑦 β†Ύ 𝐡) = 𝑧)
5857uneq1d 4126 . . . . . . . . 9 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ ((𝑦 β†Ύ 𝐡) βˆͺ {⟨𝐼, π‘˜βŸ©}) = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
5958, 38eqtr4d 2776 . . . . . . . 8 (((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 ∈ 𝐴) ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) β†’ ((𝑦 β†Ύ 𝐡) βˆͺ {⟨𝐼, π‘˜βŸ©}) = 𝑦)
6059, 52r19.29a 3156 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) β†’ ((𝑦 β†Ύ 𝐡) βˆͺ {⟨𝐼, π‘˜βŸ©}) = 𝑦)
6160adantr 482 . . . . . 6 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ ((𝑦 β†Ύ 𝐡) βˆͺ {⟨𝐼, π‘˜βŸ©}) = 𝑦)
6256, 61eqtr2d 2774 . . . . 5 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©}))
6355, 62jca 513 . . . 4 ((((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑧 = (𝑦 β†Ύ 𝐡)) β†’ (𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})))
6463anasss 468 . . 3 (((πœ‘ ∧ π‘˜ ∈ 𝐢) ∧ (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 β†Ύ 𝐡))) β†’ (𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})))
6536, 64impbida 800 . 2 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ ((𝑧 ∈ 𝐴 ∧ 𝑦 = (𝑧 βˆͺ {⟨𝐼, π‘˜βŸ©})) ↔ (𝑦 ∈ ran 𝐹 ∧ 𝑧 = (𝑦 β†Ύ 𝐡))))
664, 8, 11, 65f1od 7609 1 ((πœ‘ ∧ π‘˜ ∈ 𝐢) β†’ 𝐹:𝐴–1-1-ontoβ†’ran 𝐹)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆƒwrex 3070  Vcvv 3447   βˆͺ cun 3912   ∩ cin 3913   βŠ† wss 3914  βˆ…c0 4286  {csn 4590  βŸ¨cop 4596   ↦ cmpt 5192  ran crn 5638   β†Ύ cres 5639   Fn wfn 6495  β€“1-1-ontoβ†’wf1o 6499  (class class class)co 7361   ↑m cmap 8771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7925  df-2nd 7926  df-map 8773
This theorem is referenced by:  breprexplema  33307
  Copyright terms: Public domain W3C validator