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

Theorem cotr2g 14004
Description: Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 14005 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 5689 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
2 nfv 2009 . . . . . 6 𝑦 𝑥𝐷
3 nfv 2009 . . . . . 6 𝑧 𝑥𝐷
42, 319.21-2 2241 . . . . 5 (∀𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ (𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
54albii 1914 . . . 4 (∀𝑥𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ ∀𝑥(𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
6 simpl 474 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐵𝑦)
7 id 22 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → (𝑥𝐵𝑦𝑦𝐴𝑧))
8 simpr 477 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦𝐴𝑧)
96, 7, 83jca 1158 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
10 simp2 1167 . . . . . . . . . 10 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦𝑦𝐴𝑧))
119, 10impbii 200 . . . . . . . . 9 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
12 cotr2g.d . . . . . . . . . . . 12 dom 𝐵𝐷
13 vex 3353 . . . . . . . . . . . . 13 𝑥 ∈ V
14 vex 3353 . . . . . . . . . . . . 13 𝑦 ∈ V
1513, 14breldm 5497 . . . . . . . . . . . 12 (𝑥𝐵𝑦𝑥 ∈ dom 𝐵)
1612, 15sseldi 3759 . . . . . . . . . . 11 (𝑥𝐵𝑦𝑥𝐷)
1716pm4.71ri 556 . . . . . . . . . 10 (𝑥𝐵𝑦 ↔ (𝑥𝐷𝑥𝐵𝑦))
18 cotr2g.e . . . . . . . . . . . 12 (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸
1913, 14brelrn 5525 . . . . . . . . . . . . 13 (𝑥𝐵𝑦𝑦 ∈ ran 𝐵)
20 vex 3353 . . . . . . . . . . . . . 14 𝑧 ∈ V
2114, 20breldm 5497 . . . . . . . . . . . . 13 (𝑦𝐴𝑧𝑦 ∈ dom 𝐴)
22 elin 3958 . . . . . . . . . . . . . 14 (𝑦 ∈ (ran 𝐵 ∩ dom 𝐴) ↔ (𝑦 ∈ ran 𝐵𝑦 ∈ dom 𝐴))
2322biimpri 219 . . . . . . . . . . . . 13 ((𝑦 ∈ ran 𝐵𝑦 ∈ dom 𝐴) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
2419, 21, 23syl2an 589 . . . . . . . . . . . 12 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
2518, 24sseldi 3759 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦𝐸)
2625pm4.71ri 556 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
27 cotr2g.f . . . . . . . . . . . 12 ran 𝐴𝐹
2814, 20brelrn 5525 . . . . . . . . . . . 12 (𝑦𝐴𝑧𝑧 ∈ ran 𝐴)
2927, 28sseldi 3759 . . . . . . . . . . 11 (𝑦𝐴𝑧𝑧𝐹)
3029pm4.71ri 556 . . . . . . . . . 10 (𝑦𝐴𝑧 ↔ (𝑧𝐹𝑦𝐴𝑧))
3117, 26, 303anbi123i 1194 . . . . . . . . 9 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ ((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)))
32 3an6 1570 . . . . . . . . . 10 (((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)))
3310, 9impbii 200 . . . . . . . . . . 11 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦𝑦𝐴𝑧))
3433anbi2i 616 . . . . . . . . . 10 (((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3532, 34bitri 266 . . . . . . . . 9 (((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3611, 31, 353bitri 288 . . . . . . . 8 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3736imbi1i 340 . . . . . . 7 (((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) → 𝑥𝐶𝑧))
38 impexp 441 . . . . . . 7 ((((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) → 𝑥𝐶𝑧) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
39 3impexp 1467 . . . . . . 7 (((𝑥𝐷𝑦𝐸𝑧𝐹) → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ (𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
4037, 38, 393bitri 288 . . . . . 6 (((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
4140albii 1914 . . . . 5 (∀𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
42412albii 1915 . . . 4 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
43 df-ral 3060 . . . 4 (∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥(𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
445, 42, 433bitr4i 294 . . 3 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
45 df-ral 3060 . . . . . 6 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦(𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
46 19.21v 2034 . . . . . . . 8 (∀𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ (𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4746bicomi 215 . . . . . . 7 ((𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4847albii 1914 . . . . . 6 (∀𝑦(𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4945, 48bitri 266 . . . . 5 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
5049bicomi 215 . . . 4 (∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5150ralbii 3127 . . 3 (∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5244, 51bitri 266 . 2 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
53 df-ral 3060 . . . . 5 (∀𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5453bicomi 215 . . . 4 (∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
5554ralbii 3127 . . 3 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
5655ralbii 3127 . 2 (∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
571, 52, 563bitri 288 1 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107  wal 1650  wcel 2155  wral 3055  cin 3731  wss 3732   class class class wbr 4809  dom cdm 5277  ran crn 5278  ccom 5281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pr 5062
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-br 4810  df-opab 4872  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288
This theorem is referenced by:  cotr2  14005
  Copyright terms: Public domain W3C validator