Users' Mathboxes Mathbox for Steven Nguyen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  f1o2d2 Structured version   Visualization version   GIF version

Theorem f1o2d2 42253
Description: Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by SN, 11-Mar-2025.)
Hypotheses
Ref Expression
f1o2d2.f 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
f1o2d2.r ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶𝐷)
f1o2d2.i ((𝜑𝑧𝐷) → 𝐼𝐴)
f1o2d2.j ((𝜑𝑧𝐷) → 𝐽𝐵)
f1o2d2.1 ((𝜑 ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧𝐷)) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ 𝑧 = 𝐶))
Assertion
Ref Expression
f1o2d2 (𝜑𝐹:(𝐴 × 𝐵)–1-1-onto𝐷)
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧   𝑧,𝐶   𝑥,𝐷,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥,𝐼,𝑦   𝑥,𝐽,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦,𝑧)   𝐼(𝑧)   𝐽(𝑧)

Proof of Theorem f1o2d2
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 f1o2d2.f . . 3 𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)
2 mpompts 8089 . . 3 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑤 ∈ (𝐴 × 𝐵) ↦ (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶)
31, 2eqtri 2763 . 2 𝐹 = (𝑤 ∈ (𝐴 × 𝐵) ↦ (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶)
4 xp1st 8045 . . 3 (𝑤 ∈ (𝐴 × 𝐵) → (1st𝑤) ∈ 𝐴)
5 xp2nd 8046 . . . . . 6 (𝑤 ∈ (𝐴 × 𝐵) → (2nd𝑤) ∈ 𝐵)
6 f1o2d2.r . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶𝐷)
76anassrs 467 . . . . . . 7 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → 𝐶𝐷)
87ralrimiva 3144 . . . . . 6 ((𝜑𝑥𝐴) → ∀𝑦𝐵 𝐶𝐷)
9 rspcsbela 4444 . . . . . 6 (((2nd𝑤) ∈ 𝐵 ∧ ∀𝑦𝐵 𝐶𝐷) → (2nd𝑤) / 𝑦𝐶𝐷)
105, 8, 9syl2anr 597 . . . . 5 (((𝜑𝑥𝐴) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → (2nd𝑤) / 𝑦𝐶𝐷)
1110an32s 652 . . . 4 (((𝜑𝑤 ∈ (𝐴 × 𝐵)) ∧ 𝑥𝐴) → (2nd𝑤) / 𝑦𝐶𝐷)
1211ralrimiva 3144 . . 3 ((𝜑𝑤 ∈ (𝐴 × 𝐵)) → ∀𝑥𝐴 (2nd𝑤) / 𝑦𝐶𝐷)
13 rspcsbela 4444 . . 3 (((1st𝑤) ∈ 𝐴 ∧ ∀𝑥𝐴 (2nd𝑤) / 𝑦𝐶𝐷) → (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶𝐷)
144, 12, 13syl2an2 686 . 2 ((𝜑𝑤 ∈ (𝐴 × 𝐵)) → (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶𝐷)
15 f1o2d2.i . . 3 ((𝜑𝑧𝐷) → 𝐼𝐴)
16 f1o2d2.j . . 3 ((𝜑𝑧𝐷) → 𝐽𝐵)
1715, 16opelxpd 5728 . 2 ((𝜑𝑧𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝐴 × 𝐵))
185ad2antrl 728 . . . . 5 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → (2nd𝑤) ∈ 𝐵)
19 sbceq2g 4425 . . . . 5 ((2nd𝑤) ∈ 𝐵 → ([(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑤) / 𝑦𝐶))
2018, 19syl 17 . . . 4 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → ([(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑤) / 𝑦𝐶))
2120sbcbidv 3851 . . 3 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → ([(1st𝑤) / 𝑥][(2nd𝑤) / 𝑦]𝑧 = 𝐶[(1st𝑤) / 𝑥]𝑧 = (2nd𝑤) / 𝑦𝐶))
224ad2antrl 728 . . . 4 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → (1st𝑤) ∈ 𝐴)
2318adantr 480 . . . . 5 (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) → (2nd𝑤) ∈ 𝐵)
24 eqop 8055 . . . . . . . . 9 (𝑤 ∈ (𝐴 × 𝐵) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ ((1st𝑤) = 𝐼 ∧ (2nd𝑤) = 𝐽)))
2524ad2antrl 728 . . . . . . . 8 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ ((1st𝑤) = 𝐼 ∧ (2nd𝑤) = 𝐽)))
26 eqeq1 2739 . . . . . . . . . 10 (𝑥 = (1st𝑤) → (𝑥 = 𝐼 ↔ (1st𝑤) = 𝐼))
27 eqeq1 2739 . . . . . . . . . 10 (𝑦 = (2nd𝑤) → (𝑦 = 𝐽 ↔ (2nd𝑤) = 𝐽))
2826, 27bi2anan9 638 . . . . . . . . 9 ((𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ ((1st𝑤) = 𝐼 ∧ (2nd𝑤) = 𝐽)))
2928bicomd 223 . . . . . . . 8 ((𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → (((1st𝑤) = 𝐼 ∧ (2nd𝑤) = 𝐽) ↔ (𝑥 = 𝐼𝑦 = 𝐽)))
3025, 29sylan9bb 509 . . . . . . 7 (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ (𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤))) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ (𝑥 = 𝐼𝑦 = 𝐽)))
3130anassrs 467 . . . . . 6 ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) ∧ 𝑦 = (2nd𝑤)) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ (𝑥 = 𝐼𝑦 = 𝐽)))
32 eleq1 2827 . . . . . . . . . . . . . 14 (𝑥 = (1st𝑤) → (𝑥𝐴 ↔ (1st𝑤) ∈ 𝐴))
334, 32syl5ibrcom 247 . . . . . . . . . . . . 13 (𝑤 ∈ (𝐴 × 𝐵) → (𝑥 = (1st𝑤) → 𝑥𝐴))
3433imp 406 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑥 = (1st𝑤)) → 𝑥𝐴)
35 eleq1 2827 . . . . . . . . . . . . . 14 (𝑦 = (2nd𝑤) → (𝑦𝐵 ↔ (2nd𝑤) ∈ 𝐵))
365, 35syl5ibrcom 247 . . . . . . . . . . . . 13 (𝑤 ∈ (𝐴 × 𝐵) → (𝑦 = (2nd𝑤) → 𝑦𝐵))
3736imp 406 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 = (2nd𝑤)) → 𝑦𝐵)
3834, 37anim12dan 619 . . . . . . . . . . 11 ((𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤))) → (𝑥𝐴𝑦𝐵))
39383impb 1114 . . . . . . . . . 10 ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → (𝑥𝐴𝑦𝐵))
40393adant1r 1176 . . . . . . . . 9 (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → (𝑥𝐴𝑦𝐵))
41 simp1r 1197 . . . . . . . . 9 (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → 𝑧𝐷)
4240, 41jca 511 . . . . . . . 8 (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → ((𝑥𝐴𝑦𝐵) ∧ 𝑧𝐷))
43 f1o2d2.1 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧𝐷)) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ 𝑧 = 𝐶))
4442, 43sylan2 593 . . . . . . 7 ((𝜑 ∧ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤))) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ 𝑧 = 𝐶))
45443anassrs 1359 . . . . . 6 ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) ∧ 𝑦 = (2nd𝑤)) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ 𝑧 = 𝐶))
4631, 45bitr2d 280 . . . . 5 ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) ∧ 𝑦 = (2nd𝑤)) → (𝑧 = 𝐶𝑤 = ⟨𝐼, 𝐽⟩))
4723, 46sbcied 3837 . . . 4 (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) → ([(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑤 = ⟨𝐼, 𝐽⟩))
4822, 47sbcied 3837 . . 3 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → ([(1st𝑤) / 𝑥][(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑤 = ⟨𝐼, 𝐽⟩))
49 sbceq2g 4425 . . . 4 ((1st𝑤) ∈ 𝐴 → ([(1st𝑤) / 𝑥]𝑧 = (2nd𝑤) / 𝑦𝐶𝑧 = (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶))
5022, 49syl 17 . . 3 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → ([(1st𝑤) / 𝑥]𝑧 = (2nd𝑤) / 𝑦𝐶𝑧 = (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶))
5121, 48, 503bitr3d 309 . 2 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ 𝑧 = (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶))
523, 14, 17, 51f1o2d 7687 1 (𝜑𝐹:(𝐴 × 𝐵)–1-1-onto𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wral 3059  [wsbc 3791  csb 3908  cop 4637  cmpt 5231   × cxp 5687  1-1-ontowf1o 6562  cfv 6563  cmpo 7433  1st c1st 8011  2nd c2nd 8012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014
This theorem is referenced by:  evlselvlem  42573
  Copyright terms: Public domain W3C validator