Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mofeu Structured version   Visualization version   GIF version

Theorem mofeu 47514
Description: The uniqueness of a function into a set with at most one element. (Contributed by Zhi Wang, 1-Oct-2024.)
Hypotheses
Ref Expression
mofeu.1 𝐺 = (𝐴 Γ— 𝐡)
mofeu.2 (πœ‘ β†’ (𝐡 = βˆ… β†’ 𝐴 = βˆ…))
mofeu.3 (πœ‘ β†’ βˆƒ*π‘₯ π‘₯ ∈ 𝐡)
Assertion
Ref Expression
mofeu (πœ‘ β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹 = 𝐺))
Distinct variable group:   π‘₯,𝐡
Allowed substitution hints:   πœ‘(π‘₯)   𝐴(π‘₯)   𝐹(π‘₯)   𝐺(π‘₯)

Proof of Theorem mofeu
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 mofeu.2 . . . . 5 (πœ‘ β†’ (𝐡 = βˆ… β†’ 𝐴 = βˆ…))
21imp 408 . . . 4 ((πœ‘ ∧ 𝐡 = βˆ…) β†’ 𝐴 = βˆ…)
3 f00 6774 . . . . 5 (𝐹:π΄βŸΆβˆ… ↔ (𝐹 = βˆ… ∧ 𝐴 = βˆ…))
43rbaib 540 . . . 4 (𝐴 = βˆ… β†’ (𝐹:π΄βŸΆβˆ… ↔ 𝐹 = βˆ…))
52, 4syl 17 . . 3 ((πœ‘ ∧ 𝐡 = βˆ…) β†’ (𝐹:π΄βŸΆβˆ… ↔ 𝐹 = βˆ…))
6 feq3 6701 . . . 4 (𝐡 = βˆ… β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹:π΄βŸΆβˆ…))
76adantl 483 . . 3 ((πœ‘ ∧ 𝐡 = βˆ…) β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹:π΄βŸΆβˆ…))
8 mofeu.1 . . . . . 6 𝐺 = (𝐴 Γ— 𝐡)
9 xpeq2 5698 . . . . . . 7 (𝐡 = βˆ… β†’ (𝐴 Γ— 𝐡) = (𝐴 Γ— βˆ…))
10 xp0 6158 . . . . . . 7 (𝐴 Γ— βˆ…) = βˆ…
119, 10eqtrdi 2789 . . . . . 6 (𝐡 = βˆ… β†’ (𝐴 Γ— 𝐡) = βˆ…)
128, 11eqtrid 2785 . . . . 5 (𝐡 = βˆ… β†’ 𝐺 = βˆ…)
1312adantl 483 . . . 4 ((πœ‘ ∧ 𝐡 = βˆ…) β†’ 𝐺 = βˆ…)
1413eqeq2d 2744 . . 3 ((πœ‘ ∧ 𝐡 = βˆ…) β†’ (𝐹 = 𝐺 ↔ 𝐹 = βˆ…))
155, 7, 143bitr4d 311 . 2 ((πœ‘ ∧ 𝐡 = βˆ…) β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹 = 𝐺))
16 19.42v 1958 . . 3 (βˆƒπ‘¦(πœ‘ ∧ 𝐡 = {𝑦}) ↔ (πœ‘ ∧ βˆƒπ‘¦ 𝐡 = {𝑦}))
17 fconst2g 7204 . . . . . . . 8 (𝑦 ∈ V β†’ (𝐹:𝐴⟢{𝑦} ↔ 𝐹 = (𝐴 Γ— {𝑦})))
1817elv 3481 . . . . . . 7 (𝐹:𝐴⟢{𝑦} ↔ 𝐹 = (𝐴 Γ— {𝑦}))
19 feq3 6701 . . . . . . . 8 (𝐡 = {𝑦} β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹:𝐴⟢{𝑦}))
20 xpeq2 5698 . . . . . . . . 9 (𝐡 = {𝑦} β†’ (𝐴 Γ— 𝐡) = (𝐴 Γ— {𝑦}))
2120eqeq2d 2744 . . . . . . . 8 (𝐡 = {𝑦} β†’ (𝐹 = (𝐴 Γ— 𝐡) ↔ 𝐹 = (𝐴 Γ— {𝑦})))
2219, 21bibi12d 346 . . . . . . 7 (𝐡 = {𝑦} β†’ ((𝐹:𝐴⟢𝐡 ↔ 𝐹 = (𝐴 Γ— 𝐡)) ↔ (𝐹:𝐴⟢{𝑦} ↔ 𝐹 = (𝐴 Γ— {𝑦}))))
2318, 22mpbiri 258 . . . . . 6 (𝐡 = {𝑦} β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹 = (𝐴 Γ— 𝐡)))
248eqeq2i 2746 . . . . . 6 (𝐹 = 𝐺 ↔ 𝐹 = (𝐴 Γ— 𝐡))
2523, 24bitr4di 289 . . . . 5 (𝐡 = {𝑦} β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹 = 𝐺))
2625adantl 483 . . . 4 ((πœ‘ ∧ 𝐡 = {𝑦}) β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹 = 𝐺))
2726exlimiv 1934 . . 3 (βˆƒπ‘¦(πœ‘ ∧ 𝐡 = {𝑦}) β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹 = 𝐺))
2816, 27sylbir 234 . 2 ((πœ‘ ∧ βˆƒπ‘¦ 𝐡 = {𝑦}) β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹 = 𝐺))
29 mofeu.3 . . 3 (πœ‘ β†’ βˆƒ*π‘₯ π‘₯ ∈ 𝐡)
30 mo0sn 47500 . . 3 (βˆƒ*π‘₯ π‘₯ ∈ 𝐡 ↔ (𝐡 = βˆ… ∨ βˆƒπ‘¦ 𝐡 = {𝑦}))
3129, 30sylib 217 . 2 (πœ‘ β†’ (𝐡 = βˆ… ∨ βˆƒπ‘¦ 𝐡 = {𝑦}))
3215, 28, 31mpjaodan 958 1 (πœ‘ β†’ (𝐹:𝐴⟢𝐡 ↔ 𝐹 = 𝐺))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆƒ*wmo 2533  Vcvv 3475  βˆ…c0 4323  {csn 4629   Γ— cxp 5675  βŸΆwf 6540
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 5300  ax-nul 5307  ax-pr 5428
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-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552
This theorem is referenced by:  functhinclem1  47661  functhinclem3  47663
  Copyright terms: Public domain W3C validator