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

Theorem cotr2g 14870
Description: Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 14871 for the main application. (Contributed by RP, 22-Mar-2020.)
Hypotheses
Ref Expression
cotr2g.d dom 𝐵𝐷
cotr2g.e (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸
cotr2g.f ran 𝐴𝐹
Assertion
Ref Expression
cotr2g ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑥,𝐷,𝑦,𝑧   𝑦,𝐸,𝑧   𝑧,𝐹
Allowed substitution hints:   𝐸(𝑥)   𝐹(𝑥,𝑦)

Proof of Theorem cotr2g
StepHypRef Expression
1 cotrg 6065 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
2 nfv 1918 . . . . . 6 𝑦 𝑥𝐷
3 nfv 1918 . . . . . 6 𝑧 𝑥𝐷
42, 319.21-2 2203 . . . . 5 (∀𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ (𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
54albii 1822 . . . 4 (∀𝑥𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ ∀𝑥(𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
6 simpl 484 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐵𝑦)
7 id 22 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → (𝑥𝐵𝑦𝑦𝐴𝑧))
8 simpr 486 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦𝐴𝑧)
96, 7, 83jca 1129 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
10 simp2 1138 . . . . . . . . . 10 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦𝑦𝐴𝑧))
119, 10impbii 208 . . . . . . . . 9 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
12 cotr2g.d . . . . . . . . . . . 12 dom 𝐵𝐷
13 vex 3451 . . . . . . . . . . . . 13 𝑥 ∈ V
14 vex 3451 . . . . . . . . . . . . 13 𝑦 ∈ V
1513, 14breldm 5868 . . . . . . . . . . . 12 (𝑥𝐵𝑦𝑥 ∈ dom 𝐵)
1612, 15sselid 3946 . . . . . . . . . . 11 (𝑥𝐵𝑦𝑥𝐷)
1716pm4.71ri 562 . . . . . . . . . 10 (𝑥𝐵𝑦 ↔ (𝑥𝐷𝑥𝐵𝑦))
18 cotr2g.e . . . . . . . . . . . 12 (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸
1913, 14brelrn 5901 . . . . . . . . . . . . 13 (𝑥𝐵𝑦𝑦 ∈ ran 𝐵)
20 vex 3451 . . . . . . . . . . . . . 14 𝑧 ∈ V
2114, 20breldm 5868 . . . . . . . . . . . . 13 (𝑦𝐴𝑧𝑦 ∈ dom 𝐴)
22 elin 3930 . . . . . . . . . . . . . 14 (𝑦 ∈ (ran 𝐵 ∩ dom 𝐴) ↔ (𝑦 ∈ ran 𝐵𝑦 ∈ dom 𝐴))
2322biimpri 227 . . . . . . . . . . . . 13 ((𝑦 ∈ ran 𝐵𝑦 ∈ dom 𝐴) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
2419, 21, 23syl2an 597 . . . . . . . . . . . 12 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
2518, 24sselid 3946 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦𝐸)
2625pm4.71ri 562 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
27 cotr2g.f . . . . . . . . . . . 12 ran 𝐴𝐹
2814, 20brelrn 5901 . . . . . . . . . . . 12 (𝑦𝐴𝑧𝑧 ∈ ran 𝐴)
2927, 28sselid 3946 . . . . . . . . . . 11 (𝑦𝐴𝑧𝑧𝐹)
3029pm4.71ri 562 . . . . . . . . . 10 (𝑦𝐴𝑧 ↔ (𝑧𝐹𝑦𝐴𝑧))
3117, 26, 303anbi123i 1156 . . . . . . . . 9 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ ((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)))
32 3an6 1447 . . . . . . . . . 10 (((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)))
3310, 9impbii 208 . . . . . . . . . . 11 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦𝑦𝐴𝑧))
3433anbi2i 624 . . . . . . . . . 10 (((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3532, 34bitri 275 . . . . . . . . 9 (((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3611, 31, 353bitri 297 . . . . . . . 8 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3736imbi1i 350 . . . . . . 7 (((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) → 𝑥𝐶𝑧))
38 impexp 452 . . . . . . 7 ((((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) → 𝑥𝐶𝑧) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
39 3impexp 1359 . . . . . . 7 (((𝑥𝐷𝑦𝐸𝑧𝐹) → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ (𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
4037, 38, 393bitri 297 . . . . . 6 (((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
4140albii 1822 . . . . 5 (∀𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
42412albii 1823 . . . 4 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
43 df-ral 3062 . . . 4 (∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥(𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
445, 42, 433bitr4i 303 . . 3 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
45 df-ral 3062 . . . . . 6 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦(𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
46 19.21v 1943 . . . . . . . 8 (∀𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ (𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4746bicomi 223 . . . . . . 7 ((𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4847albii 1822 . . . . . 6 (∀𝑦(𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4945, 48bitri 275 . . . . 5 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
5049bicomi 223 . . . 4 (∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5150ralbii 3093 . . 3 (∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5244, 51bitri 275 . 2 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
53 df-ral 3062 . . . . 5 (∀𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5453bicomi 223 . . . 4 (∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
5554ralbii 3093 . . 3 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
5655ralbii 3093 . 2 (∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
571, 52, 563bitri 297 1 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088  wal 1540  wcel 2107  wral 3061  cin 3913  wss 3914   class class class wbr 5109  dom cdm 5637  ran crn 5638  ccom 5641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pr 5388
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-br 5110  df-opab 5172  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648
This theorem is referenced by:  cotr2  14871
  Copyright terms: Public domain W3C validator