MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2mpo0 Structured version   Visualization version   GIF version

Theorem 2mpo0 7651
Description: If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021.)
Hypotheses
Ref Expression
2mpo0.o 𝑂 = (𝑥𝐴, 𝑦𝐵𝐸)
2mpo0.u ((𝑋𝐴𝑌𝐵) → (𝑋𝑂𝑌) = (𝑠𝐶, 𝑡𝐷𝐹))
Assertion
Ref Expression
2mpo0 (¬ ((𝑋𝐴𝑌𝐵) ∧ (𝑆𝐶𝑇𝐷)) → (𝑆(𝑋𝑂𝑌)𝑇) = ∅)
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝐶,𝑠,𝑡   𝐷,𝑠,𝑡
Allowed substitution hints:   𝐴(𝑡,𝑠)   𝐵(𝑡,𝑠)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝑆(𝑥,𝑦,𝑡,𝑠)   𝑇(𝑥,𝑦,𝑡,𝑠)   𝐸(𝑥,𝑦,𝑡,𝑠)   𝐹(𝑥,𝑦,𝑡,𝑠)   𝑂(𝑥,𝑦,𝑡,𝑠)   𝑋(𝑥,𝑦,𝑡,𝑠)   𝑌(𝑥,𝑦,𝑡,𝑠)

Proof of Theorem 2mpo0
StepHypRef Expression
1 ianor 980 . 2 (¬ ((𝑋𝐴𝑌𝐵) ∧ (𝑆𝐶𝑇𝐷)) ↔ (¬ (𝑋𝐴𝑌𝐵) ∨ ¬ (𝑆𝐶𝑇𝐷)))
2 2mpo0.o . . . . . 6 𝑂 = (𝑥𝐴, 𝑦𝐵𝐸)
32mpondm0 7643 . . . . 5 (¬ (𝑋𝐴𝑌𝐵) → (𝑋𝑂𝑌) = ∅)
43oveqd 7422 . . . 4 (¬ (𝑋𝐴𝑌𝐵) → (𝑆(𝑋𝑂𝑌)𝑇) = (𝑆𝑇))
5 0ov 7442 . . . 4 (𝑆𝑇) = ∅
64, 5eqtrdi 2788 . . 3 (¬ (𝑋𝐴𝑌𝐵) → (𝑆(𝑋𝑂𝑌)𝑇) = ∅)
7 notnotb 314 . . . 4 ((𝑋𝐴𝑌𝐵) ↔ ¬ ¬ (𝑋𝐴𝑌𝐵))
8 2mpo0.u . . . . . . 7 ((𝑋𝐴𝑌𝐵) → (𝑋𝑂𝑌) = (𝑠𝐶, 𝑡𝐷𝐹))
98adantr 481 . . . . . 6 (((𝑋𝐴𝑌𝐵) ∧ ¬ (𝑆𝐶𝑇𝐷)) → (𝑋𝑂𝑌) = (𝑠𝐶, 𝑡𝐷𝐹))
109oveqd 7422 . . . . 5 (((𝑋𝐴𝑌𝐵) ∧ ¬ (𝑆𝐶𝑇𝐷)) → (𝑆(𝑋𝑂𝑌)𝑇) = (𝑆(𝑠𝐶, 𝑡𝐷𝐹)𝑇))
11 eqid 2732 . . . . . . 7 (𝑠𝐶, 𝑡𝐷𝐹) = (𝑠𝐶, 𝑡𝐷𝐹)
1211mpondm0 7643 . . . . . 6 (¬ (𝑆𝐶𝑇𝐷) → (𝑆(𝑠𝐶, 𝑡𝐷𝐹)𝑇) = ∅)
1312adantl 482 . . . . 5 (((𝑋𝐴𝑌𝐵) ∧ ¬ (𝑆𝐶𝑇𝐷)) → (𝑆(𝑠𝐶, 𝑡𝐷𝐹)𝑇) = ∅)
1410, 13eqtrd 2772 . . . 4 (((𝑋𝐴𝑌𝐵) ∧ ¬ (𝑆𝐶𝑇𝐷)) → (𝑆(𝑋𝑂𝑌)𝑇) = ∅)
157, 14sylanbr 582 . . 3 ((¬ ¬ (𝑋𝐴𝑌𝐵) ∧ ¬ (𝑆𝐶𝑇𝐷)) → (𝑆(𝑋𝑂𝑌)𝑇) = ∅)
166, 15jaoi3 1059 . 2 ((¬ (𝑋𝐴𝑌𝐵) ∨ ¬ (𝑆𝐶𝑇𝐷)) → (𝑆(𝑋𝑂𝑌)𝑇) = ∅)
171, 16sylbi 216 1 (¬ ((𝑋𝐴𝑌𝐵) ∧ (𝑆𝐶𝑇𝐷)) → (𝑆(𝑋𝑂𝑌)𝑇) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 845   = wceq 1541  wcel 2106  c0 4321  (class class class)co 7405  cmpo 7407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-xp 5681  df-dm 5685  df-iota 6492  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410
This theorem is referenced by:  wwlksnon0  29097
  Copyright terms: Public domain W3C validator