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 41590
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 8045 . . 3 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑤 ∈ (𝐴 × 𝐵) ↦ (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶)
31, 2eqtri 2752 . 2 𝐹 = (𝑤 ∈ (𝐴 × 𝐵) ↦ (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶)
4 xp1st 8001 . . 3 (𝑤 ∈ (𝐴 × 𝐵) → (1st𝑤) ∈ 𝐴)
5 xp2nd 8002 . . . . . 6 (𝑤 ∈ (𝐴 × 𝐵) → (2nd𝑤) ∈ 𝐵)
6 f1o2d2.r . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶𝐷)
76anassrs 467 . . . . . . 7 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → 𝐶𝐷)
87ralrimiva 3138 . . . . . 6 ((𝜑𝑥𝐴) → ∀𝑦𝐵 𝐶𝐷)
9 rspcsbela 4428 . . . . . 6 (((2nd𝑤) ∈ 𝐵 ∧ ∀𝑦𝐵 𝐶𝐷) → (2nd𝑤) / 𝑦𝐶𝐷)
105, 8, 9syl2anr 596 . . . . 5 (((𝜑𝑥𝐴) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → (2nd𝑤) / 𝑦𝐶𝐷)
1110an32s 649 . . . 4 (((𝜑𝑤 ∈ (𝐴 × 𝐵)) ∧ 𝑥𝐴) → (2nd𝑤) / 𝑦𝐶𝐷)
1211ralrimiva 3138 . . 3 ((𝜑𝑤 ∈ (𝐴 × 𝐵)) → ∀𝑥𝐴 (2nd𝑤) / 𝑦𝐶𝐷)
13 rspcsbela 4428 . . 3 (((1st𝑤) ∈ 𝐴 ∧ ∀𝑥𝐴 (2nd𝑤) / 𝑦𝐶𝐷) → (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶𝐷)
144, 12, 13syl2an2 683 . 2 ((𝜑𝑤 ∈ (𝐴 × 𝐵)) → (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶𝐷)
15 f1o2d2.i . . 3 ((𝜑𝑧𝐷) → 𝐼𝐴)
16 f1o2d2.j . . 3 ((𝜑𝑧𝐷) → 𝐽𝐵)
1715, 16opelxpd 5706 . 2 ((𝜑𝑧𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝐴 × 𝐵))
185ad2antrl 725 . . . . 5 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → (2nd𝑤) ∈ 𝐵)
19 sbceq2g 4409 . . . . 5 ((2nd𝑤) ∈ 𝐵 → ([(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑤) / 𝑦𝐶))
2018, 19syl 17 . . . 4 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → ([(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑤) / 𝑦𝐶))
2120sbcbidv 3829 . . 3 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → ([(1st𝑤) / 𝑥][(2nd𝑤) / 𝑦]𝑧 = 𝐶[(1st𝑤) / 𝑥]𝑧 = (2nd𝑤) / 𝑦𝐶))
224ad2antrl 725 . . . 4 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → (1st𝑤) ∈ 𝐴)
2318adantr 480 . . . . 5 (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) → (2nd𝑤) ∈ 𝐵)
24 eqop 8011 . . . . . . . . 9 (𝑤 ∈ (𝐴 × 𝐵) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ ((1st𝑤) = 𝐼 ∧ (2nd𝑤) = 𝐽)))
2524ad2antrl 725 . . . . . . . 8 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ ((1st𝑤) = 𝐼 ∧ (2nd𝑤) = 𝐽)))
26 eqeq1 2728 . . . . . . . . . 10 (𝑥 = (1st𝑤) → (𝑥 = 𝐼 ↔ (1st𝑤) = 𝐼))
27 eqeq1 2728 . . . . . . . . . 10 (𝑦 = (2nd𝑤) → (𝑦 = 𝐽 ↔ (2nd𝑤) = 𝐽))
2826, 27bi2anan9 636 . . . . . . . . 9 ((𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ ((1st𝑤) = 𝐼 ∧ (2nd𝑤) = 𝐽)))
2928bicomd 222 . . . . . . . 8 ((𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → (((1st𝑤) = 𝐼 ∧ (2nd𝑤) = 𝐽) ↔ (𝑥 = 𝐼𝑦 = 𝐽)))
3025, 29sylan9bb 509 . . . . . . 7 (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ (𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤))) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ (𝑥 = 𝐼𝑦 = 𝐽)))
3130anassrs 467 . . . . . 6 ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) ∧ 𝑦 = (2nd𝑤)) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ (𝑥 = 𝐼𝑦 = 𝐽)))
32 eleq1 2813 . . . . . . . . . . . . . 14 (𝑥 = (1st𝑤) → (𝑥𝐴 ↔ (1st𝑤) ∈ 𝐴))
334, 32syl5ibrcom 246 . . . . . . . . . . . . 13 (𝑤 ∈ (𝐴 × 𝐵) → (𝑥 = (1st𝑤) → 𝑥𝐴))
3433imp 406 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑥 = (1st𝑤)) → 𝑥𝐴)
35 eleq1 2813 . . . . . . . . . . . . . 14 (𝑦 = (2nd𝑤) → (𝑦𝐵 ↔ (2nd𝑤) ∈ 𝐵))
365, 35syl5ibrcom 246 . . . . . . . . . . . . 13 (𝑤 ∈ (𝐴 × 𝐵) → (𝑦 = (2nd𝑤) → 𝑦𝐵))
3736imp 406 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 = (2nd𝑤)) → 𝑦𝐵)
3834, 37anim12dan 618 . . . . . . . . . . 11 ((𝑤 ∈ (𝐴 × 𝐵) ∧ (𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤))) → (𝑥𝐴𝑦𝐵))
39383impb 1112 . . . . . . . . . 10 ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → (𝑥𝐴𝑦𝐵))
40393adant1r 1174 . . . . . . . . 9 (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → (𝑥𝐴𝑦𝐵))
41 simp1r 1195 . . . . . . . . 9 (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → 𝑧𝐷)
4240, 41jca 511 . . . . . . . 8 (((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤)) → ((𝑥𝐴𝑦𝐵) ∧ 𝑧𝐷))
43 f1o2d2.1 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝐴𝑦𝐵) ∧ 𝑧𝐷)) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ 𝑧 = 𝐶))
4442, 43sylan2 592 . . . . . . 7 ((𝜑 ∧ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤))) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ 𝑧 = 𝐶))
45443anassrs 1357 . . . . . 6 ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) ∧ 𝑦 = (2nd𝑤)) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ 𝑧 = 𝐶))
4631, 45bitr2d 280 . . . . 5 ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) ∧ 𝑦 = (2nd𝑤)) → (𝑧 = 𝐶𝑤 = ⟨𝐼, 𝐽⟩))
4723, 46sbcied 3815 . . . 4 (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) → ([(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑤 = ⟨𝐼, 𝐽⟩))
4822, 47sbcied 3815 . . 3 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → ([(1st𝑤) / 𝑥][(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑤 = ⟨𝐼, 𝐽⟩))
49 sbceq2g 4409 . . . 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 7654 1 (𝜑𝐹:(𝐴 × 𝐵)–1-1-onto𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wral 3053  [wsbc 3770  csb 3886  cop 4627  cmpt 5222   × cxp 5665  1-1-ontowf1o 6533  cfv 6534  cmpo 7404  1st c1st 7967  2nd c2nd 7968
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418  ax-un 7719
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-oprab 7406  df-mpo 7407  df-1st 7969  df-2nd 7970
This theorem is referenced by:  evlselvlem  41689
  Copyright terms: Public domain W3C validator