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 41362
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 8055 . . 3 (𝑥𝐴, 𝑦𝐵𝐶) = (𝑤 ∈ (𝐴 × 𝐵) ↦ (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶)
31, 2eqtri 2759 . 2 𝐹 = (𝑤 ∈ (𝐴 × 𝐵) ↦ (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶)
4 xp1st 8011 . . 3 (𝑤 ∈ (𝐴 × 𝐵) → (1st𝑤) ∈ 𝐴)
5 xp2nd 8012 . . . . . 6 (𝑤 ∈ (𝐴 × 𝐵) → (2nd𝑤) ∈ 𝐵)
6 f1o2d2.r . . . . . . . 8 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝐶𝐷)
76anassrs 467 . . . . . . 7 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → 𝐶𝐷)
87ralrimiva 3145 . . . . . 6 ((𝜑𝑥𝐴) → ∀𝑦𝐵 𝐶𝐷)
9 rspcsbela 4435 . . . . . 6 (((2nd𝑤) ∈ 𝐵 ∧ ∀𝑦𝐵 𝐶𝐷) → (2nd𝑤) / 𝑦𝐶𝐷)
105, 8, 9syl2anr 596 . . . . 5 (((𝜑𝑥𝐴) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → (2nd𝑤) / 𝑦𝐶𝐷)
1110an32s 649 . . . 4 (((𝜑𝑤 ∈ (𝐴 × 𝐵)) ∧ 𝑥𝐴) → (2nd𝑤) / 𝑦𝐶𝐷)
1211ralrimiva 3145 . . 3 ((𝜑𝑤 ∈ (𝐴 × 𝐵)) → ∀𝑥𝐴 (2nd𝑤) / 𝑦𝐶𝐷)
13 rspcsbela 4435 . . 3 (((1st𝑤) ∈ 𝐴 ∧ ∀𝑥𝐴 (2nd𝑤) / 𝑦𝐶𝐷) → (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶𝐷)
144, 12, 13syl2an2 683 . 2 ((𝜑𝑤 ∈ (𝐴 × 𝐵)) → (1st𝑤) / 𝑥(2nd𝑤) / 𝑦𝐶𝐷)
15 f1o2d2.i . . 3 ((𝜑𝑧𝐷) → 𝐼𝐴)
16 f1o2d2.j . . 3 ((𝜑𝑧𝐷) → 𝐽𝐵)
1715, 16opelxpd 5715 . 2 ((𝜑𝑧𝐷) → ⟨𝐼, 𝐽⟩ ∈ (𝐴 × 𝐵))
185ad2antrl 725 . . . . 5 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → (2nd𝑤) ∈ 𝐵)
19 sbceq2g 4416 . . . . 5 ((2nd𝑤) ∈ 𝐵 → ([(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑤) / 𝑦𝐶))
2018, 19syl 17 . . . 4 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → ([(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑧 = (2nd𝑤) / 𝑦𝐶))
2120sbcbidv 3836 . . 3 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → ([(1st𝑤) / 𝑥][(2nd𝑤) / 𝑦]𝑧 = 𝐶[(1st𝑤) / 𝑥]𝑧 = (2nd𝑤) / 𝑦𝐶))
224ad2antrl 725 . . . 4 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → (1st𝑤) ∈ 𝐴)
2318adantr 480 . . . . 5 (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) → (2nd𝑤) ∈ 𝐵)
24 eqop 8021 . . . . . . . . 9 (𝑤 ∈ (𝐴 × 𝐵) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ ((1st𝑤) = 𝐼 ∧ (2nd𝑤) = 𝐽)))
2524ad2antrl 725 . . . . . . . 8 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → (𝑤 = ⟨𝐼, 𝐽⟩ ↔ ((1st𝑤) = 𝐼 ∧ (2nd𝑤) = 𝐽)))
26 eqeq1 2735 . . . . . . . . . 10 (𝑥 = (1st𝑤) → (𝑥 = 𝐼 ↔ (1st𝑤) = 𝐼))
27 eqeq1 2735 . . . . . . . . . 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 2820 . . . . . . . . . . . . . 14 (𝑥 = (1st𝑤) → (𝑥𝐴 ↔ (1st𝑤) ∈ 𝐴))
334, 32syl5ibrcom 246 . . . . . . . . . . . . 13 (𝑤 ∈ (𝐴 × 𝐵) → (𝑥 = (1st𝑤) → 𝑥𝐴))
3433imp 406 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑥 = (1st𝑤)) → 𝑥𝐴)
35 eleq1 2820 . . . . . . . . . . . . . 14 (𝑦 = (2nd𝑤) → (𝑦𝐵 ↔ (2nd𝑤) ∈ 𝐵))
365, 35syl5ibrcom 246 . . . . . . . . . . . . 13 (𝑤 ∈ (𝐴 × 𝐵) → (𝑦 = (2nd𝑤) → 𝑦𝐵))
3736imp 406 . . . . . . . . . . . 12 ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑦 = (2nd𝑤)) → 𝑦𝐵)
3834, 37anim12dan 618 . . . . . . . . . . 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 592 . . . . . . 7 ((𝜑 ∧ ((𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷) ∧ 𝑥 = (1st𝑤) ∧ 𝑦 = (2nd𝑤))) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ 𝑧 = 𝐶))
45443anassrs 1359 . . . . . 6 ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) ∧ 𝑦 = (2nd𝑤)) → ((𝑥 = 𝐼𝑦 = 𝐽) ↔ 𝑧 = 𝐶))
4631, 45bitr2d 280 . . . . 5 ((((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) ∧ 𝑦 = (2nd𝑤)) → (𝑧 = 𝐶𝑤 = ⟨𝐼, 𝐽⟩))
4723, 46sbcied 3822 . . . 4 (((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) ∧ 𝑥 = (1st𝑤)) → ([(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑤 = ⟨𝐼, 𝐽⟩))
4822, 47sbcied 3822 . . 3 ((𝜑 ∧ (𝑤 ∈ (𝐴 × 𝐵) ∧ 𝑧𝐷)) → ([(1st𝑤) / 𝑥][(2nd𝑤) / 𝑦]𝑧 = 𝐶𝑤 = ⟨𝐼, 𝐽⟩))
49 sbceq2g 4416 . . . 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 7664 1 (𝜑𝐹:(𝐴 × 𝐵)–1-1-onto𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1086   = wceq 1540  wcel 2105  wral 3060  [wsbc 3777  csb 3893  cop 4634  cmpt 5231   × cxp 5674  1-1-ontowf1o 6542  cfv 6543  cmpo 7414  1st c1st 7977  2nd c2nd 7978
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 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980
This theorem is referenced by:  evlselvlem  41461
  Copyright terms: Public domain W3C validator