ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fnmpoovd GIF version

Theorem fnmpoovd 6115
Description: A function with a Cartesian product as domain is a mapping with two arguments defined by its operation values. (Contributed by AV, 20-Feb-2019.) (Revised by AV, 3-Jul-2022.)
Hypotheses
Ref Expression
fnmpoovd.m (𝜑𝑀 Fn (𝐴 × 𝐵))
fnmpoovd.s ((𝑖 = 𝑎𝑗 = 𝑏) → 𝐷 = 𝐶)
fnmpoovd.d ((𝜑𝑖𝐴𝑗𝐵) → 𝐷𝑈)
fnmpoovd.c ((𝜑𝑎𝐴𝑏𝐵) → 𝐶𝑉)
Assertion
Ref Expression
fnmpoovd (𝜑 → (𝑀 = (𝑎𝐴, 𝑏𝐵𝐶) ↔ ∀𝑖𝐴𝑗𝐵 (𝑖𝑀𝑗) = 𝐷))
Distinct variable groups:   𝐴,𝑎,𝑏,𝑖,𝑗   𝐵,𝑎,𝑏,𝑖,𝑗   𝐶,𝑖,𝑗   𝐷,𝑎,𝑏   𝑖,𝑀,𝑗   𝜑,𝑎,𝑏,𝑖,𝑗
Allowed substitution hints:   𝐶(𝑎,𝑏)   𝐷(𝑖,𝑗)   𝑈(𝑖,𝑗,𝑎,𝑏)   𝑀(𝑎,𝑏)   𝑉(𝑖,𝑗,𝑎,𝑏)

Proof of Theorem fnmpoovd
StepHypRef Expression
1 fnmpoovd.m . . 3 (𝜑𝑀 Fn (𝐴 × 𝐵))
2 fnmpoovd.c . . . . . 6 ((𝜑𝑎𝐴𝑏𝐵) → 𝐶𝑉)
323expb 1182 . . . . 5 ((𝜑 ∧ (𝑎𝐴𝑏𝐵)) → 𝐶𝑉)
43ralrimivva 2514 . . . 4 (𝜑 → ∀𝑎𝐴𝑏𝐵 𝐶𝑉)
5 eqid 2139 . . . . 5 (𝑎𝐴, 𝑏𝐵𝐶) = (𝑎𝐴, 𝑏𝐵𝐶)
65fnmpo 6103 . . . 4 (∀𝑎𝐴𝑏𝐵 𝐶𝑉 → (𝑎𝐴, 𝑏𝐵𝐶) Fn (𝐴 × 𝐵))
74, 6syl 14 . . 3 (𝜑 → (𝑎𝐴, 𝑏𝐵𝐶) Fn (𝐴 × 𝐵))
8 eqfnov2 5881 . . 3 ((𝑀 Fn (𝐴 × 𝐵) ∧ (𝑎𝐴, 𝑏𝐵𝐶) Fn (𝐴 × 𝐵)) → (𝑀 = (𝑎𝐴, 𝑏𝐵𝐶) ↔ ∀𝑖𝐴𝑗𝐵 (𝑖𝑀𝑗) = (𝑖(𝑎𝐴, 𝑏𝐵𝐶)𝑗)))
91, 7, 8syl2anc 408 . 2 (𝜑 → (𝑀 = (𝑎𝐴, 𝑏𝐵𝐶) ↔ ∀𝑖𝐴𝑗𝐵 (𝑖𝑀𝑗) = (𝑖(𝑎𝐴, 𝑏𝐵𝐶)𝑗)))
10 nfcv 2281 . . . . . . . 8 𝑎𝐷
11 nfcv 2281 . . . . . . . 8 𝑏𝐷
12 nfcv 2281 . . . . . . . 8 𝑖𝐶
13 nfcv 2281 . . . . . . . 8 𝑗𝐶
14 fnmpoovd.s . . . . . . . 8 ((𝑖 = 𝑎𝑗 = 𝑏) → 𝐷 = 𝐶)
1510, 11, 12, 13, 14cbvmpo 5853 . . . . . . 7 (𝑖𝐴, 𝑗𝐵𝐷) = (𝑎𝐴, 𝑏𝐵𝐶)
1615eqcomi 2143 . . . . . 6 (𝑎𝐴, 𝑏𝐵𝐶) = (𝑖𝐴, 𝑗𝐵𝐷)
1716a1i 9 . . . . 5 (𝜑 → (𝑎𝐴, 𝑏𝐵𝐶) = (𝑖𝐴, 𝑗𝐵𝐷))
1817oveqd 5794 . . . 4 (𝜑 → (𝑖(𝑎𝐴, 𝑏𝐵𝐶)𝑗) = (𝑖(𝑖𝐴, 𝑗𝐵𝐷)𝑗))
1918eqeq2d 2151 . . 3 (𝜑 → ((𝑖𝑀𝑗) = (𝑖(𝑎𝐴, 𝑏𝐵𝐶)𝑗) ↔ (𝑖𝑀𝑗) = (𝑖(𝑖𝐴, 𝑗𝐵𝐷)𝑗)))
20192ralbidv 2459 . 2 (𝜑 → (∀𝑖𝐴𝑗𝐵 (𝑖𝑀𝑗) = (𝑖(𝑎𝐴, 𝑏𝐵𝐶)𝑗) ↔ ∀𝑖𝐴𝑗𝐵 (𝑖𝑀𝑗) = (𝑖(𝑖𝐴, 𝑗𝐵𝐷)𝑗)))
21 simprl 520 . . . . 5 ((𝜑 ∧ (𝑖𝐴𝑗𝐵)) → 𝑖𝐴)
22 simprr 521 . . . . 5 ((𝜑 ∧ (𝑖𝐴𝑗𝐵)) → 𝑗𝐵)
23 fnmpoovd.d . . . . . 6 ((𝜑𝑖𝐴𝑗𝐵) → 𝐷𝑈)
24233expb 1182 . . . . 5 ((𝜑 ∧ (𝑖𝐴𝑗𝐵)) → 𝐷𝑈)
25 eqid 2139 . . . . . 6 (𝑖𝐴, 𝑗𝐵𝐷) = (𝑖𝐴, 𝑗𝐵𝐷)
2625ovmpt4g 5896 . . . . 5 ((𝑖𝐴𝑗𝐵𝐷𝑈) → (𝑖(𝑖𝐴, 𝑗𝐵𝐷)𝑗) = 𝐷)
2721, 22, 24, 26syl3anc 1216 . . . 4 ((𝜑 ∧ (𝑖𝐴𝑗𝐵)) → (𝑖(𝑖𝐴, 𝑗𝐵𝐷)𝑗) = 𝐷)
2827eqeq2d 2151 . . 3 ((𝜑 ∧ (𝑖𝐴𝑗𝐵)) → ((𝑖𝑀𝑗) = (𝑖(𝑖𝐴, 𝑗𝐵𝐷)𝑗) ↔ (𝑖𝑀𝑗) = 𝐷))
29282ralbidva 2457 . 2 (𝜑 → (∀𝑖𝐴𝑗𝐵 (𝑖𝑀𝑗) = (𝑖(𝑖𝐴, 𝑗𝐵𝐷)𝑗) ↔ ∀𝑖𝐴𝑗𝐵 (𝑖𝑀𝑗) = 𝐷))
309, 20, 293bitrd 213 1 (𝜑 → (𝑀 = (𝑎𝐴, 𝑏𝐵𝐶) ↔ ∀𝑖𝐴𝑗𝐵 (𝑖𝑀𝑗) = 𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 962   = wceq 1331  wcel 1480  wral 2416   × cxp 4540   Fn wfn 5121  (class class class)co 5777  cmpo 5779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4049  ax-pow 4101  ax-pr 4134  ax-un 4358  ax-setind 4455
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3740  df-iun 3818  df-br 3933  df-opab 3993  df-mpt 3994  df-id 4218  df-xp 4548  df-rel 4549  df-cnv 4550  df-co 4551  df-dm 4552  df-rn 4553  df-res 4554  df-ima 4555  df-iota 5091  df-fun 5128  df-fn 5129  df-f 5130  df-fv 5134  df-ov 5780  df-oprab 5781  df-mpo 5782  df-1st 6041  df-2nd 6042
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator