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 46427
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 407 . . . 4 ((𝜑𝐵 = ∅) → 𝐴 = ∅)
3 f00 6693 . . . . 5 (𝐹:𝐴⟶∅ ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
43rbaib 539 . . . 4 (𝐴 = ∅ → (𝐹:𝐴⟶∅ ↔ 𝐹 = ∅))
52, 4syl 17 . . 3 ((𝜑𝐵 = ∅) → (𝐹:𝐴⟶∅ ↔ 𝐹 = ∅))
6 feq3 6620 . . . 4 (𝐵 = ∅ → (𝐹:𝐴𝐵𝐹:𝐴⟶∅))
76adantl 482 . . 3 ((𝜑𝐵 = ∅) → (𝐹:𝐴𝐵𝐹:𝐴⟶∅))
8 mofeu.1 . . . . . 6 𝐺 = (𝐴 × 𝐵)
9 xpeq2 5628 . . . . . . 7 (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
10 xp0 6083 . . . . . . 7 (𝐴 × ∅) = ∅
119, 10eqtrdi 2793 . . . . . 6 (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
128, 11eqtrid 2789 . . . . 5 (𝐵 = ∅ → 𝐺 = ∅)
1312adantl 482 . . . 4 ((𝜑𝐵 = ∅) → 𝐺 = ∅)
1413eqeq2d 2748 . . 3 ((𝜑𝐵 = ∅) → (𝐹 = 𝐺𝐹 = ∅))
155, 7, 143bitr4d 310 . 2 ((𝜑𝐵 = ∅) → (𝐹:𝐴𝐵𝐹 = 𝐺))
16 19.42v 1956 . . 3 (∃𝑦(𝜑𝐵 = {𝑦}) ↔ (𝜑 ∧ ∃𝑦 𝐵 = {𝑦}))
17 fconst2g 7117 . . . . . . . 8 (𝑦 ∈ V → (𝐹:𝐴⟶{𝑦} ↔ 𝐹 = (𝐴 × {𝑦})))
1817elv 3447 . . . . . . 7 (𝐹:𝐴⟶{𝑦} ↔ 𝐹 = (𝐴 × {𝑦}))
19 feq3 6620 . . . . . . . 8 (𝐵 = {𝑦} → (𝐹:𝐴𝐵𝐹:𝐴⟶{𝑦}))
20 xpeq2 5628 . . . . . . . . 9 (𝐵 = {𝑦} → (𝐴 × 𝐵) = (𝐴 × {𝑦}))
2120eqeq2d 2748 . . . . . . . 8 (𝐵 = {𝑦} → (𝐹 = (𝐴 × 𝐵) ↔ 𝐹 = (𝐴 × {𝑦})))
2219, 21bibi12d 345 . . . . . . 7 (𝐵 = {𝑦} → ((𝐹:𝐴𝐵𝐹 = (𝐴 × 𝐵)) ↔ (𝐹:𝐴⟶{𝑦} ↔ 𝐹 = (𝐴 × {𝑦}))))
2318, 22mpbiri 257 . . . . . 6 (𝐵 = {𝑦} → (𝐹:𝐴𝐵𝐹 = (𝐴 × 𝐵)))
248eqeq2i 2750 . . . . . 6 (𝐹 = 𝐺𝐹 = (𝐴 × 𝐵))
2523, 24bitr4di 288 . . . . 5 (𝐵 = {𝑦} → (𝐹:𝐴𝐵𝐹 = 𝐺))
2625adantl 482 . . . 4 ((𝜑𝐵 = {𝑦}) → (𝐹:𝐴𝐵𝐹 = 𝐺))
2726exlimiv 1932 . . 3 (∃𝑦(𝜑𝐵 = {𝑦}) → (𝐹:𝐴𝐵𝐹 = 𝐺))
2816, 27sylbir 234 . 2 ((𝜑 ∧ ∃𝑦 𝐵 = {𝑦}) → (𝐹:𝐴𝐵𝐹 = 𝐺))
29 mofeu.3 . . 3 (𝜑 → ∃*𝑥 𝑥𝐵)
30 mo0sn 46413 . . 3 (∃*𝑥 𝑥𝐵 ↔ (𝐵 = ∅ ∨ ∃𝑦 𝐵 = {𝑦}))
3129, 30sylib 217 . 2 (𝜑 → (𝐵 = ∅ ∨ ∃𝑦 𝐵 = {𝑦}))
3215, 28, 31mpjaodan 956 1 (𝜑 → (𝐹:𝐴𝐵𝐹 = 𝐺))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 844   = wceq 1540  wex 1780  wcel 2105  ∃*wmo 2537  Vcvv 3441  c0 4267  {csn 4571   × cxp 5605  wf 6461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-mpt 5171  df-id 5507  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-fv 6473
This theorem is referenced by:  functhinclem1  46574  functhinclem3  46576
  Copyright terms: Public domain W3C validator