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

Theorem cotr2g 14853
Description: Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 14854 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 6059 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
2 nfv 1917 . . . . . 6 𝑦 𝑥𝐷
3 nfv 1917 . . . . . 6 𝑧 𝑥𝐷
42, 319.21-2 2202 . . . . 5 (∀𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ (𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
54albii 1821 . . . 4 (∀𝑥𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ ∀𝑥(𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
6 simpl 483 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐵𝑦)
7 id 22 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → (𝑥𝐵𝑦𝑦𝐴𝑧))
8 simpr 485 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦𝐴𝑧)
96, 7, 83jca 1128 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
10 simp2 1137 . . . . . . . . . 10 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦𝑦𝐴𝑧))
119, 10impbii 208 . . . . . . . . 9 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
12 cotr2g.d . . . . . . . . . . . 12 dom 𝐵𝐷
13 vex 3447 . . . . . . . . . . . . 13 𝑥 ∈ V
14 vex 3447 . . . . . . . . . . . . 13 𝑦 ∈ V
1513, 14breldm 5862 . . . . . . . . . . . 12 (𝑥𝐵𝑦𝑥 ∈ dom 𝐵)
1612, 15sselid 3940 . . . . . . . . . . 11 (𝑥𝐵𝑦𝑥𝐷)
1716pm4.71ri 561 . . . . . . . . . 10 (𝑥𝐵𝑦 ↔ (𝑥𝐷𝑥𝐵𝑦))
18 cotr2g.e . . . . . . . . . . . 12 (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸
1913, 14brelrn 5895 . . . . . . . . . . . . 13 (𝑥𝐵𝑦𝑦 ∈ ran 𝐵)
20 vex 3447 . . . . . . . . . . . . . 14 𝑧 ∈ V
2114, 20breldm 5862 . . . . . . . . . . . . 13 (𝑦𝐴𝑧𝑦 ∈ dom 𝐴)
22 elin 3924 . . . . . . . . . . . . . 14 (𝑦 ∈ (ran 𝐵 ∩ dom 𝐴) ↔ (𝑦 ∈ ran 𝐵𝑦 ∈ dom 𝐴))
2322biimpri 227 . . . . . . . . . . . . 13 ((𝑦 ∈ ran 𝐵𝑦 ∈ dom 𝐴) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
2419, 21, 23syl2an 596 . . . . . . . . . . . 12 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
2518, 24sselid 3940 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑦𝐸)
2625pm4.71ri 561 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
27 cotr2g.f . . . . . . . . . . . 12 ran 𝐴𝐹
2814, 20brelrn 5895 . . . . . . . . . . . 12 (𝑦𝐴𝑧𝑧 ∈ ran 𝐴)
2927, 28sselid 3940 . . . . . . . . . . 11 (𝑦𝐴𝑧𝑧𝐹)
3029pm4.71ri 561 . . . . . . . . . 10 (𝑦𝐴𝑧 ↔ (𝑧𝐹𝑦𝐴𝑧))
3117, 26, 303anbi123i 1155 . . . . . . . . 9 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ ((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)))
32 3an6 1446 . . . . . . . . . 10 (((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)))
3310, 9impbii 208 . . . . . . . . . . 11 ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦𝑦𝐴𝑧))
3433anbi2i 623 . . . . . . . . . 10 (((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3532, 34bitri 274 . . . . . . . . 9 (((𝑥𝐷𝑥𝐵𝑦) ∧ (𝑦𝐸 ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) ∧ (𝑧𝐹𝑦𝐴𝑧)) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3611, 31, 353bitri 296 . . . . . . . 8 ((𝑥𝐵𝑦𝑦𝐴𝑧) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)))
3736imbi1i 349 . . . . . . 7 (((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) → 𝑥𝐶𝑧))
38 impexp 451 . . . . . . 7 ((((𝑥𝐷𝑦𝐸𝑧𝐹) ∧ (𝑥𝐵𝑦𝑦𝐴𝑧)) → 𝑥𝐶𝑧) ↔ ((𝑥𝐷𝑦𝐸𝑧𝐹) → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
39 3impexp 1358 . . . . . . 7 (((𝑥𝐷𝑦𝐸𝑧𝐹) → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ (𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
4037, 38, 393bitri 296 . . . . . 6 (((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
4140albii 1821 . . . . 5 (∀𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
42412albii 1822 . . . 4 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝑦𝑧(𝑥𝐷 → (𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
43 df-ral 3063 . . . 4 (∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥(𝑥𝐷 → ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
445, 42, 433bitr4i 302 . . 3 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
45 df-ral 3063 . . . . . 6 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦(𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
46 19.21v 1942 . . . . . . . 8 (∀𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ (𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4746bicomi 223 . . . . . . 7 ((𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4847albii 1821 . . . . . 6 (∀𝑦(𝑦𝐸 → ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
4945, 48bitri 274 . . . . 5 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
5049bicomi 223 . . . 4 (∀𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5150ralbii 3094 . . 3 (∀𝑥𝐷𝑦𝑧(𝑦𝐸 → (𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5244, 51bitri 274 . 2 (∀𝑥𝑦𝑧((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
53 df-ral 3063 . . . . 5 (∀𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
5453bicomi 223 . . . 4 (∀𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
5554ralbii 3094 . . 3 (∀𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
5655ralbii 3094 . 2 (∀𝑥𝐷𝑦𝐸𝑧(𝑧𝐹 → ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
571, 52, 563bitri 296 1 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥𝐷𝑦𝐸𝑧𝐹 ((𝑥𝐵𝑦𝑦𝐴𝑧) → 𝑥𝐶𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087  wal 1539  wcel 2106  wral 3062  cin 3907  wss 3908   class class class wbr 5103  dom cdm 5631  ran crn 5632  ccom 5635
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2707  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5166  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642
This theorem is referenced by:  cotr2  14854
  Copyright terms: Public domain W3C validator