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

Theorem cotr2g 13657
Description: Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 13658 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 5471 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
2 nfv 1840 . . . . . 6 𝑦 𝑥𝐷
3 nfv 1840 . . . . . 6 𝑧 𝑥𝐷
42, 319.21-2 2076 . . . . 5 (∀𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ (𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
54albii 1744 . . . 4 (∀𝑥𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ ∀𝑥(𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
6 simpl 473 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐵𝑦)
7 id 22 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → (𝑥𝐵𝑦𝑦𝐴𝑧))
8 simpr 477 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦𝐴𝑧)
96, 7, 83jca 1240 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
10 simp2 1060 . . . . . . . . . 10 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦𝑦𝐴𝑧))
119, 10impbii 199 . . . . . . . . 9 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
12 cotr2g.d . . . . . . . . . . . 12 dom 𝐵𝐷
13 vex 3192 . . . . . . . . . . . . 13 𝑥 ∈ V
14 vex 3192 . . . . . . . . . . . . 13 𝑦 ∈ V
1513, 14breldm 5294 . . . . . . . . . . . 12 (𝑥𝐵𝑦𝑥 ∈ dom 𝐵)
1612, 15sseldi 3585 . . . . . . . . . . 11 (𝑥𝐵𝑦𝑥𝐷)
1716pm4.71ri 664 . . . . . . . . . 10 (𝑥𝐵𝑦 ↔ (𝑥𝐷𝑥𝐵𝑦))
18 cotr2g.e . . . . . . . . . . . 12 (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸
1913, 14brelrn 5321 . . . . . . . . . . . . 13 (𝑥𝐵𝑦𝑦 ∈ ran 𝐵)
20 vex 3192 . . . . . . . . . . . . . 14 𝑧 ∈ V
2114, 20breldm 5294 . . . . . . . . . . . . 13 (𝑦𝐴𝑧𝑦 ∈ dom 𝐴)
22 elin 3779 . . . . . . . . . . . . . 14 (𝑦 ∈ (ran 𝐵 ∩ dom 𝐴) ↔ (𝑦 ∈ ran 𝐵𝑦 ∈ dom 𝐴))
2322biimpri 218 . . . . . . . . . . . . 13 ((𝑦 ∈ ran 𝐵𝑦 ∈ dom 𝐴) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
2419, 21, 23syl2an 494 . . . . . . . . . . . 12 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
2518, 24sseldi 3585 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦𝐸)
2625pm4.71ri 664 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
27 cotr2g.f . . . . . . . . . . . 12 ran 𝐴𝐹
2814, 20brelrn 5321 . . . . . . . . . . . 12 (𝑦𝐴𝑧𝑧 ∈ ran 𝐴)
2927, 28sseldi 3585 . . . . . . . . . . 11 (𝑦𝐴𝑧𝑧𝐹)
3029pm4.71ri 664 . . . . . . . . . 10 (𝑦𝐴𝑧 ↔ (𝑧𝐹𝑦𝐴𝑧))
3117, 26, 303anbi123i 1249 . . . . . . . . 9 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ ((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)))
32 3an6 1406 . . . . . . . . . 10 (((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)))
3310, 9impbii 199 . . . . . . . . . . 11 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦𝑦𝐴𝑧))
3433anbi2i 729 . . . . . . . . . 10 (((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3532, 34bitri 264 . . . . . . . . 9 (((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3611, 31, 353bitri 286 . . . . . . . 8 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3736imbi1i 339 . . . . . . 7 (((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) → 𝑥𝐶𝑧))
38 impexp 462 . . . . . . 7 ((((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) → 𝑥𝐶𝑧) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
39 3impexp 1286 . . . . . . 7 (((𝑥𝐷𝑦𝐸𝑧𝐹) → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ (𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
4037, 38, 393bitri 286 . . . . . 6 (((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
4140albii 1744 . . . . 5 (∀𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
42412albii 1745 . . . 4 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
43 df-ral 2912 . . . 4 (∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥(𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
445, 42, 433bitr4i 292 . . 3 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
45 df-ral 2912 . . . . . 6 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦(𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
46 19.21v 1865 . . . . . . . 8 (∀𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ (𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4746bicomi 214 . . . . . . 7 ((𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4847albii 1744 . . . . . 6 (∀𝑦(𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4945, 48bitri 264 . . . . 5 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
5049bicomi 214 . . . 4 (∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5150ralbii 2975 . . 3 (∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5244, 51bitri 264 . 2 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
53 df-ral 2912 . . . . 5 (∀𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5453bicomi 214 . . . 4 (∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
5554ralbii 2975 . . 3 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
5655ralbii 2975 . 2 (∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
571, 52, 563bitri 286 1 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036  wal 1478  wcel 1987  wral 2907  cin 3558  wss 3559   class class class wbr 4618  dom cdm 5079  ran crn 5080  ccom 5083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-br 4619  df-opab 4679  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090
This theorem is referenced by:  cotr2  13658
  Copyright terms: Public domain W3C validator