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 ∈ F x B y ∧ y A z → x C z

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 ∀ z x B y ∧ y A z → x C z
5 nfv ⊢ Ⅎ y x ∈ D
6 nfv ⊢ Ⅎ z x ∈ D
7 5 6 19.21-2 ⊢ ∀ y ∀ z x ∈ D → y ∈ E → z ∈ F → x B y ∧ y A z → x C z ↔ x ∈ D → ∀ y ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z
8 7 albii ⊢ ∀ x ∀ y ∀ z x ∈ D → y ∈ E → z ∈ F → x B y ∧ y A z → x C z ↔ ∀ x x ∈ D → ∀ y ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z
9 simpl ⊢ x B y ∧ y A z → x B y
10 id ⊢ x B y ∧ y A z → x B y ∧ y A z
11 simpr ⊢ x B y ∧ y A z → y A z
12 9 10 11 3jca ⊢ x B y ∧ y A z → x B y ∧ x B y ∧ y A z ∧ y A z
13 simp2 ⊢ x B y ∧ x B y ∧ y A z ∧ y A z → x B y ∧ y A z
14 12 13 impbii ⊢ x B y ∧ y A z ↔ x B y ∧ x B y ∧ y A z ∧ y A z
15 vex ⊢ x ∈ V
16 vex ⊢ y ∈ V
17 15 16 breldm ⊢ x B y → x ∈ dom ⁡ B
18 1 17 sselid ⊢ x B y → x ∈ D
19 18 pm4.71ri ⊢ x B y ↔ x ∈ D ∧ x B y
20 15 16 brelrn ⊢ x B y → y ∈ ran ⁡ B
21 vex ⊢ z ∈ V
22 16 21 breldm ⊢ y A z → 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 ⊢ x B y ∧ y A z → y ∈ ran ⁡ B ∩ dom ⁡ A
26 2 25 sselid ⊢ x B y ∧ y A z → y ∈ E
27 26 pm4.71ri ⊢ x B y ∧ y A z ↔ y ∈ E ∧ x B y ∧ y A z
28 16 21 brelrn ⊢ y A z → z ∈ ran ⁡ A
29 3 28 sselid ⊢ y A z → z ∈ F
30 29 pm4.71ri ⊢ y A z ↔ z ∈ F ∧ y A z
31 19 27 30 3anbi123i ⊢ x B y ∧ x B y ∧ y A z ∧ y A z ↔ x ∈ D ∧ x B y ∧ y ∈ E ∧ x B y ∧ y A z ∧ z ∈ F ∧ y A z
32 3an6 ⊢ x ∈ D ∧ x B y ∧ y ∈ E ∧ x B y ∧ y A z ∧ z ∈ F ∧ y A z ↔ x ∈ D ∧ y ∈ E ∧ z ∈ F ∧ x B y ∧ x B y ∧ y A z ∧ y A z
33 13 12 impbii ⊢ x B y ∧ x B y ∧ y A z ∧ y A z ↔ x B y ∧ y A z
34 33 anbi2i ⊢ x ∈ D ∧ y ∈ E ∧ z ∈ F ∧ x B y ∧ x B y ∧ y A z ∧ y A z ↔ x ∈ D ∧ y ∈ E ∧ z ∈ F ∧ x B y ∧ y A z
35 32 34 bitri ⊢ x ∈ D ∧ x B y ∧ y ∈ E ∧ x B y ∧ y A z ∧ z ∈ F ∧ y A z ↔ x ∈ D ∧ y ∈ E ∧ z ∈ F ∧ x B y ∧ y A z
36 14 31 35 3bitri ⊢ x B y ∧ y A z ↔ x ∈ D ∧ y ∈ E ∧ z ∈ F ∧ x B y ∧ y A z
37 36 imbi1i ⊢ x B y ∧ y A z → x C z ↔ x ∈ D ∧ y ∈ E ∧ z ∈ F ∧ x B y ∧ y A z → x C z
38 impexp ⊢ x ∈ D ∧ y ∈ E ∧ z ∈ F ∧ x B y ∧ y A z → x C z ↔ x ∈ D ∧ y ∈ E ∧ z ∈ F → x B y ∧ y A z → x C z
39 3impexp ⊢ x ∈ D ∧ y ∈ E ∧ z ∈ F → x B y ∧ y A z → x C z ↔ x ∈ D → y ∈ E → z ∈ F → x B y ∧ y A z → x C z
40 37 38 39 3bitri ⊢ x B y ∧ y A z → x C z ↔ x ∈ D → y ∈ E → z ∈ F → x B y ∧ y A z → x C z
41 40 albii ⊢ ∀ z x B y ∧ y A z → x C z ↔ ∀ z x ∈ D → y ∈ E → z ∈ F → x B y ∧ y A z → x C z
42 41 2albii ⊢ ∀ x ∀ y ∀ z x B y ∧ y A z → x C z ↔ ∀ x ∀ y ∀ z x ∈ D → y ∈ E → z ∈ F → x B y ∧ y A z → x C z
43 df-ral ⊢ ∀ x ∈ D ∀ y ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z ↔ ∀ x x ∈ D → ∀ y ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z
44 8 42 43 3bitr4i ⊢ ∀ x ∀ y ∀ z x B y ∧ y A z → x C z ↔ ∀ x ∈ D ∀ y ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z
45 df-ral ⊢ ∀ y ∈ E ∀ z z ∈ F → x B y ∧ y A z → x C z ↔ ∀ y y ∈ E → ∀ z z ∈ F → x B y ∧ y A z → x C z
46 19.21v ⊢ ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z ↔ y ∈ E → ∀ z z ∈ F → x B y ∧ y A z → x C z
47 46 bicomi ⊢ y ∈ E → ∀ z z ∈ F → x B y ∧ y A z → x C z ↔ ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z
48 47 albii ⊢ ∀ y y ∈ E → ∀ z z ∈ F → x B y ∧ y A z → x C z ↔ ∀ y ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z
49 45 48 bitri ⊢ ∀ y ∈ E ∀ z z ∈ F → x B y ∧ y A z → x C z ↔ ∀ y ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z
50 49 bicomi ⊢ ∀ y ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z ↔ ∀ y ∈ E ∀ z z ∈ F → x B y ∧ y A z → x C z
51 50 ralbii ⊢ ∀ x ∈ D ∀ y ∀ z y ∈ E → z ∈ F → x B y ∧ y A z → x C z ↔ ∀ x ∈ D ∀ y ∈ E ∀ z z ∈ F → x B y ∧ y A z → x C z
52 44 51 bitri ⊢ ∀ x ∀ y ∀ z x B y ∧ y A z → x C z ↔ ∀ x ∈ D ∀ y ∈ E ∀ z z ∈ F → x B y ∧ y A z → x C z
53 df-ral ⊢ ∀ z ∈ F x B y ∧ y A z → x C z ↔ ∀ z z ∈ F → x B y ∧ y A z → x C z
54 53 bicomi ⊢ ∀ z z ∈ F → x B y ∧ y A z → x C z ↔ ∀ z ∈ F x B y ∧ y A z → x C z
55 54 ralbii ⊢ ∀ y ∈ E ∀ z z ∈ F → x B y ∧ y A z → x C z ↔ ∀ y ∈ E ∀ z ∈ F x B y ∧ y A z → x C z
56 55 ralbii ⊢ ∀ x ∈ D ∀ y ∈ E ∀ z z ∈ F → x B y ∧ y A z → x C z ↔ ∀ x ∈ D ∀ y ∈ E ∀ z ∈ F x B y ∧ y A z → x C z
57 4 52 56 3bitri ⊢ A ∘ B ⊆ C ↔ ∀ x ∈ D ∀ y ∈ E ∀ z ∈ F x B y ∧ y A z → x C z