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 𝐵 ⊆ 𝐷
cotr2g.e ⊢ ( ran 𝐵 ∩ dom 𝐴 ) ⊆ 𝐸
cotr2g.f ⊢ ran 𝐴 ⊆ 𝐹
Assertion cotr2g ( ( 𝐴 ∘ 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ∈ 𝐹 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )

Proof

Step Hyp Ref Expression
1 cotr2g.d ⊢ dom 𝐵 ⊆ 𝐷
2 cotr2g.e ⊢ ( ran 𝐵 ∩ dom 𝐴 ) ⊆ 𝐸
3 cotr2g.f ⊢ ran 𝐴 ⊆ 𝐹
4 cotrg ⊢ ( ( 𝐴 ∘ 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
5 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐷
6 nfv ⊢ Ⅎ 𝑧 𝑥 ∈ 𝐷
7 5 6 19.21-2 ⊢ ( ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐷 → ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ) ↔ ( 𝑥 ∈ 𝐷 → ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ) )
8 7 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐷 → ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐷 → ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ) )
9 simpl ⊢ ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐵 𝑦 )
10 id ⊢ ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
11 simpr ⊢ ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑦 𝐴 𝑧 )
12 9 10 11 3jca ⊢ ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → ( 𝑥 𝐵 𝑦 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) )
13 simp2 ⊢ ( ( 𝑥 𝐵 𝑦 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) → ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
14 12 13 impbii ⊢ ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ↔ ( 𝑥 𝐵 𝑦 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) )
15 vex ⊢ 𝑥 ∈ V
16 vex ⊢ 𝑦 ∈ V
17 15 16 breldm ⊢ ( 𝑥 𝐵 𝑦 → 𝑥 ∈ dom 𝐵 )
18 1 17 sselid ⊢ ( 𝑥 𝐵 𝑦 → 𝑥 ∈ 𝐷 )
19 18 pm4.71ri ⊢ ( 𝑥 𝐵 𝑦 ↔ ( 𝑥 ∈ 𝐷 ∧ 𝑥 𝐵 𝑦 ) )
20 15 16 brelrn ⊢ ( 𝑥 𝐵 𝑦 → 𝑦 ∈ ran 𝐵 )
21 vex ⊢ 𝑧 ∈ V
22 16 21 breldm ⊢ ( 𝑦 𝐴 𝑧 → 𝑦 ∈ dom 𝐴 )
23 elin ⊢ ( 𝑦 ∈ ( ran 𝐵 ∩ dom 𝐴 ) ↔ ( 𝑦 ∈ ran 𝐵 ∧ 𝑦 ∈ dom 𝐴 ) )
24 23 biimpri ⊢ ( ( 𝑦 ∈ ran 𝐵 ∧ 𝑦 ∈ dom 𝐴 ) → 𝑦 ∈ ( ran 𝐵 ∩ dom 𝐴 ) )
25 20 22 24 syl2an ⊢ ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑦 ∈ ( ran 𝐵 ∩ dom 𝐴 ) )
26 2 25 sselid ⊢ ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑦 ∈ 𝐸 )
27 26 pm4.71ri ⊢ ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ↔ ( 𝑦 ∈ 𝐸 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
28 16 21 brelrn ⊢ ( 𝑦 𝐴 𝑧 → 𝑧 ∈ ran 𝐴 )
29 3 28 sselid ⊢ ( 𝑦 𝐴 𝑧 → 𝑧 ∈ 𝐹 )
30 29 pm4.71ri ⊢ ( 𝑦 𝐴 𝑧 ↔ ( 𝑧 ∈ 𝐹 ∧ 𝑦 𝐴 𝑧 ) )
31 19 27 30 3anbi123i ⊢ ( ( 𝑥 𝐵 𝑦 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 𝐵 𝑦 ) ∧ ( 𝑦 ∈ 𝐸 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑦 𝐴 𝑧 ) ) )
32 3an6 ⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 𝐵 𝑦 ) ∧ ( 𝑦 ∈ 𝐸 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑦 𝐴 𝑧 ) ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹 ) ∧ ( 𝑥 𝐵 𝑦 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) ) )
33 13 12 impbii ⊢ ( ( 𝑥 𝐵 𝑦 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) ↔ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
34 33 anbi2i ⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹 ) ∧ ( 𝑥 𝐵 𝑦 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ∧ 𝑦 𝐴 𝑧 ) ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹 ) ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
35 32 34 bitri ⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑥 𝐵 𝑦 ) ∧ ( 𝑦 ∈ 𝐸 ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑦 𝐴 𝑧 ) ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹 ) ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
36 14 31 35 3bitri ⊢ ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹 ) ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
37 36 imbi1i ⊢ ( ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹 ) ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) → 𝑥 𝐶 𝑧 ) )
38 impexp ⊢ ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹 ) ∧ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) → 𝑥 𝐶 𝑧 ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹 ) → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) )
39 3impexp ⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹 ) → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐷 → ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ) )
40 37 38 39 3bitri ⊢ ( ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ( 𝑥 ∈ 𝐷 → ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ) )
41 40 albii ⊢ ( ∀ 𝑧 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑧 ( 𝑥 ∈ 𝐷 → ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ) )
42 41 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝑥 ∈ 𝐷 → ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ) )
43 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐷 → ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ) )
44 8 42 43 3bitr4i ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) )
45 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐸 → ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) )
46 19.21v ⊢ ( ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ↔ ( 𝑦 ∈ 𝐸 → ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) )
47 46 bicomi ⊢ ( ( 𝑦 ∈ 𝐸 → ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ↔ ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) )
48 47 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐸 → ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ↔ ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) )
49 45 48 bitri ⊢ ( ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ↔ ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) )
50 49 bicomi ⊢ ( ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ↔ ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) )
51 50 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝐸 → ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) )
52 44 51 bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) )
53 df-ral ⊢ ( ∀ 𝑧 ∈ 𝐹 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) )
54 53 bicomi ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐹 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
55 54 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ∈ 𝐹 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
56 55 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ( 𝑧 ∈ 𝐹 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ∈ 𝐹 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
57 4 52 56 3bitri ⊢ ( ( 𝐴 ∘ 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐸 ∀ 𝑧 ∈ 𝐹 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )