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

Theorem el2mpt2cl 7236
 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. Using implicit substitution. (Contributed by AV, 21-May-2021.)
Hypotheses
Ref Expression
el2mpt2cl.o 𝑂 = (𝑥𝐴, 𝑦𝐵 ↦ (𝑠𝐶, 𝑡𝐷𝐸))
el2mpt2cl.e ((𝑥 = 𝑋𝑦 = 𝑌) → (𝐶 = 𝐹𝐷 = 𝐺))
Assertion
Ref Expression
el2mpt2cl (∀𝑥𝐴𝑦𝐵 (𝐶𝑈𝐷𝑉) → (𝑊 ∈ (𝑆(𝑋𝑂𝑌)𝑇) → ((𝑋𝐴𝑌𝐵) ∧ (𝑆𝐹𝑇𝐺))))
Distinct variable groups:   𝐴,𝑠,𝑡,𝑥,𝑦   𝐵,𝑠,𝑡,𝑥,𝑦   𝐶,𝑠,𝑡   𝐷,𝑠,𝑡   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦   𝑥,𝑈,𝑦   𝑥,𝑉,𝑦   𝑋,𝑠,𝑡,𝑥,𝑦   𝑌,𝑠,𝑡,𝑥,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝑆(𝑥,𝑦,𝑡,𝑠)   𝑇(𝑥,𝑦,𝑡,𝑠)   𝑈(𝑡,𝑠)   𝐸(𝑥,𝑦,𝑡,𝑠)   𝐹(𝑡,𝑠)   𝐺(𝑡,𝑠)   𝑂(𝑥,𝑦,𝑡,𝑠)   𝑉(𝑡,𝑠)   𝑊(𝑥,𝑦,𝑡,𝑠)

Proof of Theorem el2mpt2cl
StepHypRef Expression
1 el2mpt2cl.o . . 3 𝑂 = (𝑥𝐴, 𝑦𝐵 ↦ (𝑠𝐶, 𝑡𝐷𝐸))
21el2mpt2csbcl 7235 . 2 (∀𝑥𝐴𝑦𝐵 (𝐶𝑈𝐷𝑉) → (𝑊 ∈ (𝑆(𝑋𝑂𝑌)𝑇) → ((𝑋𝐴𝑌𝐵) ∧ (𝑆𝑋 / 𝑥𝑌 / 𝑦𝐶𝑇𝑋 / 𝑥𝑌 / 𝑦𝐷))))
3 simpl 473 . . . . . . 7 ((𝑋𝐴𝑌𝐵) → 𝑋𝐴)
4 simplr 791 . . . . . . . 8 (((𝑋𝐴𝑌𝐵) ∧ 𝑥 = 𝑋) → 𝑌𝐵)
5 el2mpt2cl.e . . . . . . . . . 10 ((𝑥 = 𝑋𝑦 = 𝑌) → (𝐶 = 𝐹𝐷 = 𝐺))
65simpld 475 . . . . . . . . 9 ((𝑥 = 𝑋𝑦 = 𝑌) → 𝐶 = 𝐹)
76adantll 749 . . . . . . . 8 ((((𝑋𝐴𝑌𝐵) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝐶 = 𝐹)
84, 7csbied 3553 . . . . . . 7 (((𝑋𝐴𝑌𝐵) ∧ 𝑥 = 𝑋) → 𝑌 / 𝑦𝐶 = 𝐹)
93, 8csbied 3553 . . . . . 6 ((𝑋𝐴𝑌𝐵) → 𝑋 / 𝑥𝑌 / 𝑦𝐶 = 𝐹)
109eleq2d 2685 . . . . 5 ((𝑋𝐴𝑌𝐵) → (𝑆𝑋 / 𝑥𝑌 / 𝑦𝐶𝑆𝐹))
115simprd 479 . . . . . . . . 9 ((𝑥 = 𝑋𝑦 = 𝑌) → 𝐷 = 𝐺)
1211adantll 749 . . . . . . . 8 ((((𝑋𝐴𝑌𝐵) ∧ 𝑥 = 𝑋) ∧ 𝑦 = 𝑌) → 𝐷 = 𝐺)
134, 12csbied 3553 . . . . . . 7 (((𝑋𝐴𝑌𝐵) ∧ 𝑥 = 𝑋) → 𝑌 / 𝑦𝐷 = 𝐺)
143, 13csbied 3553 . . . . . 6 ((𝑋𝐴𝑌𝐵) → 𝑋 / 𝑥𝑌 / 𝑦𝐷 = 𝐺)
1514eleq2d 2685 . . . . 5 ((𝑋𝐴𝑌𝐵) → (𝑇𝑋 / 𝑥𝑌 / 𝑦𝐷𝑇𝐺))
1610, 15anbi12d 746 . . . 4 ((𝑋𝐴𝑌𝐵) → ((𝑆𝑋 / 𝑥𝑌 / 𝑦𝐶𝑇𝑋 / 𝑥𝑌 / 𝑦𝐷) ↔ (𝑆𝐹𝑇𝐺)))
1716biimpd 219 . . 3 ((𝑋𝐴𝑌𝐵) → ((𝑆𝑋 / 𝑥𝑌 / 𝑦𝐶𝑇𝑋 / 𝑥𝑌 / 𝑦𝐷) → (𝑆𝐹𝑇𝐺)))
1817imdistani 725 . 2 (((𝑋𝐴𝑌𝐵) ∧ (𝑆𝑋 / 𝑥𝑌 / 𝑦𝐶𝑇𝑋 / 𝑥𝑌 / 𝑦𝐷)) → ((𝑋𝐴𝑌𝐵) ∧ (𝑆𝐹𝑇𝐺)))
192, 18syl6 35 1 (∀𝑥𝐴𝑦𝐵 (𝐶𝑈𝐷𝑉) → (𝑊 ∈ (𝑆(𝑋𝑂𝑌)𝑇) → ((𝑋𝐴𝑌𝐵) ∧ (𝑆𝐹𝑇𝐺))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1481   ∈ wcel 1988  ∀wral 2909  ⦋csb 3526  (class class class)co 6635   ↦ cmpt2 6637 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-1st 7153  df-2nd 7154 This theorem is referenced by:  wspthnonp  26725
 Copyright terms: Public domain W3C validator