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

Theorem cotr2g 14331
Description: Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 14332 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 5942 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
2 nfv 1915 . . . . . 6 𝑦 𝑥𝐷
3 nfv 1915 . . . . . 6 𝑧 𝑥𝐷
42, 319.21-2 2208 . . . . 5 (∀𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ (𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
54albii 1821 . . . 4 (∀𝑥𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ ∀𝑥(𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
6 simpl 486 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐵𝑦)
7 id 22 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → (𝑥𝐵𝑦𝑦𝐴𝑧))
8 simpr 488 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦𝐴𝑧)
96, 7, 83jca 1125 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
10 simp2 1134 . . . . . . . . . 10 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦𝑦𝐴𝑧))
119, 10impbii 212 . . . . . . . . 9 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
12 cotr2g.d . . . . . . . . . . . 12 dom 𝐵𝐷
13 vex 3447 . . . . . . . . . . . . 13 𝑥 ∈ V
14 vex 3447 . . . . . . . . . . . . 13 𝑦 ∈ V
1513, 14breldm 5745 . . . . . . . . . . . 12 (𝑥𝐵𝑦𝑥 ∈ dom 𝐵)
1612, 15sseldi 3916 . . . . . . . . . . 11 (𝑥𝐵𝑦𝑥𝐷)
1716pm4.71ri 564 . . . . . . . . . 10 (𝑥𝐵𝑦 ↔ (𝑥𝐷𝑥𝐵𝑦))
18 cotr2g.e . . . . . . . . . . . 12 (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸
1913, 14brelrn 5780 . . . . . . . . . . . . 13 (𝑥𝐵𝑦𝑦 ∈ ran 𝐵)
20 vex 3447 . . . . . . . . . . . . . 14 𝑧 ∈ V
2114, 20breldm 5745 . . . . . . . . . . . . 13 (𝑦𝐴𝑧𝑦 ∈ dom 𝐴)
22 elin 3900 . . . . . . . . . . . . . 14 (𝑦 ∈ (ran 𝐵 ∩ dom 𝐴) ↔ (𝑦 ∈ ran 𝐵𝑦 ∈ dom 𝐴))
2322biimpri 231 . . . . . . . . . . . . 13 ((𝑦 ∈ ran 𝐵𝑦 ∈ dom 𝐴) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
2419, 21, 23syl2an 598 . . . . . . . . . . . 12 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
2518, 24sseldi 3916 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦𝐸)
2625pm4.71ri 564 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
27 cotr2g.f . . . . . . . . . . . 12 ran 𝐴𝐹
2814, 20brelrn 5780 . . . . . . . . . . . 12 (𝑦𝐴𝑧𝑧 ∈ ran 𝐴)
2927, 28sseldi 3916 . . . . . . . . . . 11 (𝑦𝐴𝑧𝑧𝐹)
3029pm4.71ri 564 . . . . . . . . . 10 (𝑦𝐴𝑧 ↔ (𝑧𝐹𝑦𝐴𝑧))
3117, 26, 303anbi123i 1152 . . . . . . . . 9 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ ((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)))
32 3an6 1443 . . . . . . . . . 10 (((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)))
3310, 9impbii 212 . . . . . . . . . . 11 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦𝑦𝐴𝑧))
3433anbi2i 625 . . . . . . . . . 10 (((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3532, 34bitri 278 . . . . . . . . 9 (((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3611, 31, 353bitri 300 . . . . . . . 8 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3736imbi1i 353 . . . . . . 7 (((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) → 𝑥𝐶𝑧))
38 impexp 454 . . . . . . 7 ((((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) → 𝑥𝐶𝑧) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
39 3impexp 1355 . . . . . . 7 (((𝑥𝐷𝑦𝐸𝑧𝐹) → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ (𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
4037, 38, 393bitri 300 . . . . . 6 (((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
4140albii 1821 . . . . 5 (∀𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
42412albii 1822 . . . 4 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
43 df-ral 3114 . . . 4 (∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥(𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
445, 42, 433bitr4i 306 . . 3 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
45 df-ral 3114 . . . . . 6 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦(𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
46 19.21v 1940 . . . . . . . 8 (∀𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ (𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4746bicomi 227 . . . . . . 7 ((𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4847albii 1821 . . . . . 6 (∀𝑦(𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4945, 48bitri 278 . . . . 5 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
5049bicomi 227 . . . 4 (∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5150ralbii 3136 . . 3 (∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5244, 51bitri 278 . 2 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
53 df-ral 3114 . . . . 5 (∀𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5453bicomi 227 . . . 4 (∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
5554ralbii 3136 . . 3 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
5655ralbii 3136 . 2 (∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
571, 52, 563bitri 300 1 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084  wal 1536  wcel 2112  wral 3109  cin 3883  wss 3884   class class class wbr 5033  dom cdm 5523  ran crn 5524  ccom 5527
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534
This theorem is referenced by:  cotr2  14332
  Copyright terms: Public domain W3C validator