Metamath Proof Explorer

Theorem cotr2g

Description: Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 for the main application. (Contributed by RP, 22-Mar-2020)

Ref Expression
Hypotheses cotr2g.d ⊢dom⁡B⊆D
cotr2g.e ⊢ran⁡B∩dom⁡A⊆E
cotr2g.f ⊢ran⁡A⊆F
Assertion cotr2g ⊢A∘B⊆C↔∀x∈D∀y∈E∀z∈FxBy∧yAz→xCz

Proof

Step Hyp Ref Expression
1 cotr2g.d ⊢dom⁡B⊆D
2 cotr2g.e ⊢ran⁡B∩dom⁡A⊆E
3 cotr2g.f ⊢ran⁡A⊆F
4 cotrg ⊢A∘B⊆C↔∀x∀y∀zxBy∧yAz→xCz
5 nfv ⊢Ⅎyx∈D
6 nfv ⊢Ⅎzx∈D
7 5 6 19.21-2 ⊢∀y∀zx∈D→y∈E→z∈F→xBy∧yAz→xCz↔x∈D→∀y∀zy∈E→z∈F→xBy∧yAz→xCz
8 7 albii ⊢∀x∀y∀zx∈D→y∈E→z∈F→xBy∧yAz→xCz↔∀xx∈D→∀y∀zy∈E→z∈F→xBy∧yAz→xCz
9 simpl ⊢xBy∧yAz→xBy
10 id ⊢xBy∧yAz→xBy∧yAz
11 simpr ⊢xBy∧yAz→yAz
12 9 10 11 3jca ⊢xBy∧yAz→xBy∧xBy∧yAz∧yAz
13 simp2 ⊢xBy∧xBy∧yAz∧yAz→xBy∧yAz
14 12 13 impbii ⊢xBy∧yAz↔xBy∧xBy∧yAz∧yAz
15 vex ⊢x∈V
16 vex ⊢y∈V
17 15 16 breldm ⊢xBy→x∈dom⁡B
18 1 17 sselid ⊢xBy→x∈D
19 18 pm4.71ri ⊢xBy↔x∈D∧xBy
20 15 16 brelrn ⊢xBy→y∈ran⁡B
21 vex ⊢z∈V
22 16 21 breldm ⊢yAz→y∈dom⁡A
23 elin ⊢y∈ran⁡B∩dom⁡A↔y∈ran⁡B∧y∈dom⁡A
24 23 biimpri ⊢y∈ran⁡B∧y∈dom⁡A→y∈ran⁡B∩dom⁡A
25 20 22 24 syl2an ⊢xBy∧yAz→y∈ran⁡B∩dom⁡A
26 2 25 sselid ⊢xBy∧yAz→y∈E
27 26 pm4.71ri ⊢xBy∧yAz↔y∈E∧xBy∧yAz
28 16 21 brelrn ⊢yAz→z∈ran⁡A
29 3 28 sselid ⊢yAz→z∈F
30 29 pm4.71ri ⊢yAz↔z∈F∧yAz
31 19 27 30 3anbi123i ⊢xBy∧xBy∧yAz∧yAz↔x∈D∧xBy∧y∈E∧xBy∧yAz∧z∈F∧yAz
32 3an6 ⊢x∈D∧xBy∧y∈E∧xBy∧yAz∧z∈F∧yAz↔x∈D∧y∈E∧z∈F∧xBy∧xBy∧yAz∧yAz
33 13 12 impbii ⊢xBy∧xBy∧yAz∧yAz↔xBy∧yAz
34 33 anbi2i ⊢x∈D∧y∈E∧z∈F∧xBy∧xBy∧yAz∧yAz↔x∈D∧y∈E∧z∈F∧xBy∧yAz
35 32 34 bitri ⊢x∈D∧xBy∧y∈E∧xBy∧yAz∧z∈F∧yAz↔x∈D∧y∈E∧z∈F∧xBy∧yAz
36 14 31 35 3bitri ⊢xBy∧yAz↔x∈D∧y∈E∧z∈F∧xBy∧yAz
37 36 imbi1i ⊢xBy∧yAz→xCz↔x∈D∧y∈E∧z∈F∧xBy∧yAz→xCz
38 impexp ⊢x∈D∧y∈E∧z∈F∧xBy∧yAz→xCz↔x∈D∧y∈E∧z∈F→xBy∧yAz→xCz
39 3impexp ⊢x∈D∧y∈E∧z∈F→xBy∧yAz→xCz↔x∈D→y∈E→z∈F→xBy∧yAz→xCz
40 37 38 39 3bitri ⊢xBy∧yAz→xCz↔x∈D→y∈E→z∈F→xBy∧yAz→xCz
41 40 albii ⊢∀zxBy∧yAz→xCz↔∀zx∈D→y∈E→z∈F→xBy∧yAz→xCz
42 41 2albii ⊢∀x∀y∀zxBy∧yAz→xCz↔∀x∀y∀zx∈D→y∈E→z∈F→xBy∧yAz→xCz
43 df-ral ⊢∀x∈D∀y∀zy∈E→z∈F→xBy∧yAz→xCz↔∀xx∈D→∀y∀zy∈E→z∈F→xBy∧yAz→xCz
44 8 42 43 3bitr4i ⊢∀x∀y∀zxBy∧yAz→xCz↔∀x∈D∀y∀zy∈E→z∈F→xBy∧yAz→xCz
45 df-ral ⊢∀y∈E∀zz∈F→xBy∧yAz→xCz↔∀yy∈E→∀zz∈F→xBy∧yAz→xCz
46 19.21v ⊢∀zy∈E→z∈F→xBy∧yAz→xCz↔y∈E→∀zz∈F→xBy∧yAz→xCz
47 46 bicomi ⊢y∈E→∀zz∈F→xBy∧yAz→xCz↔∀zy∈E→z∈F→xBy∧yAz→xCz
48 47 albii ⊢∀yy∈E→∀zz∈F→xBy∧yAz→xCz↔∀y∀zy∈E→z∈F→xBy∧yAz→xCz
49 45 48 bitri ⊢∀y∈E∀zz∈F→xBy∧yAz→xCz↔∀y∀zy∈E→z∈F→xBy∧yAz→xCz
50 49 bicomi ⊢∀y∀zy∈E→z∈F→xBy∧yAz→xCz↔∀y∈E∀zz∈F→xBy∧yAz→xCz
51 50 ralbii ⊢∀x∈D∀y∀zy∈E→z∈F→xBy∧yAz→xCz↔∀x∈D∀y∈E∀zz∈F→xBy∧yAz→xCz
52 44 51 bitri ⊢∀x∀y∀zxBy∧yAz→xCz↔∀x∈D∀y∈E∀zz∈F→xBy∧yAz→xCz
53 df-ral ⊢∀z∈FxBy∧yAz→xCz↔∀zz∈F→xBy∧yAz→xCz
54 53 bicomi ⊢∀zz∈F→xBy∧yAz→xCz↔∀z∈FxBy∧yAz→xCz
55 54 ralbii ⊢∀y∈E∀zz∈F→xBy∧yAz→xCz↔∀y∈E∀z∈FxBy∧yAz→xCz
56 55 ralbii ⊢∀x∈D∀y∈E∀zz∈F→xBy∧yAz→xCz↔∀x∈D∀y∈E∀z∈FxBy∧yAz→xCz
57 4 52 56 3bitri ⊢A∘B⊆C↔∀x∈D∀y∈E∀z∈FxBy∧yAz→xCz