cotr2g - Metamath Proof Explorer

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

Theorem cotr2g 14336

Description: Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 14337 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**
Step	Hyp	Ref	Expression
1		cotrg 5971	. 2 ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
2		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐷
3		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑧 𝑥 ∈ 𝐷
4	2, 3	19.21-2 2209	. . . . 5 ⊢ (∀𝑦∀𝑧(𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ (𝑥 ∈ 𝐷 → ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
5	4	albii 1820	. . . 4 ⊢ (∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
6		simpl 485	. . . . . . . . . . 11 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐵𝑦)
7		id 22	. . . . . . . . . . 11 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))
8		simpr 487	. . . . . . . . . . 11 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑦𝐴𝑧)
9	6, 7, 8	3jca 1124	. . . . . . . . . 10 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
10		simp2 1133	. . . . . . . . . 10 ⊢ ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))
11	9, 10	impbii 211	. . . . . . . . 9 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
12		cotr2g.d	. . . . . . . . . . . 12 ⊢ dom 𝐵 ⊆ 𝐷
13		vex 3497	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
14		vex 3497	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
15	13, 14	breldm 5777	. . . . . . . . . . . 12 ⊢ (𝑥𝐵𝑦 → 𝑥 ∈ dom 𝐵)
16	12, 15	sseldi 3965	. . . . . . . . . . 11 ⊢ (𝑥𝐵𝑦 → 𝑥 ∈ 𝐷)
17	16	pm4.71ri 563	. . . . . . . . . 10 ⊢ (𝑥𝐵𝑦 ↔ (𝑥 ∈ 𝐷 ∧ 𝑥𝐵𝑦))
18		cotr2g.e	. . . . . . . . . . . 12 ⊢ (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸
19	13, 14	brelrn 5812	. . . . . . . . . . . . 13 ⊢ (𝑥𝐵𝑦 → 𝑦 ∈ ran 𝐵)
20		vex 3497	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
21	14, 20	breldm 5777	. . . . . . . . . . . . 13 ⊢ (𝑦𝐴𝑧 → 𝑦 ∈ dom 𝐴)
22		elin 4169	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (ran 𝐵 ∩ dom 𝐴) ↔ (𝑦 ∈ ran 𝐵 ∧ 𝑦 ∈ dom 𝐴))
23	22	biimpri 230	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ran 𝐵 ∧ 𝑦 ∈ dom 𝐴) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
24	19, 21, 23	syl2an 597	. . . . . . . . . . . 12 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
25	18, 24	sseldi 3965	. . . . . . . . . . 11 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑦 ∈ 𝐸)
26	25	pm4.71ri 563	. . . . . . . . . 10 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ↔ (𝑦 ∈ 𝐸 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
27		cotr2g.f	. . . . . . . . . . . 12 ⊢ ran 𝐴 ⊆ 𝐹
28	14, 20	brelrn 5812	. . . . . . . . . . . 12 ⊢ (𝑦𝐴𝑧 → 𝑧 ∈ ran 𝐴)
29	27, 28	sseldi 3965	. . . . . . . . . . 11 ⊢ (𝑦𝐴𝑧 → 𝑧 ∈ 𝐹)
30	29	pm4.71ri 563	. . . . . . . . . 10 ⊢ (𝑦𝐴𝑧 ↔ (𝑧 ∈ 𝐹 ∧ 𝑦𝐴𝑧))
31	17, 26, 30	3anbi123i 1151	. . . . . . . . 9 ⊢ ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑥𝐵𝑦) ∧ (𝑦 ∈ 𝐸 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦𝐴𝑧)))
32		3an6 1442	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑥𝐵𝑦) ∧ (𝑦 ∈ 𝐸 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦𝐴𝑧)) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)))
33	10, 9	impbii 211	. . . . . . . . . . 11 ⊢ ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))
34	33	anbi2i 624	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
35	32, 34	bitri 277	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑥𝐵𝑦) ∧ (𝑦 ∈ 𝐸 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦𝐴𝑧)) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
36	11, 31, 35	3bitri 299	. . . . . . . 8 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
37	36	imbi1i 352	. . . . . . 7 ⊢ (((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) → 𝑥𝐶𝑧))
38		impexp 453	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) → 𝑥𝐶𝑧) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
39		3impexp 1354	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ (𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
40	37, 38, 39	3bitri 299	. . . . . 6 ⊢ (((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
41	40	albii 1820	. . . . 5 ⊢ (∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
42	41	2albii 1821	. . . 4 ⊢ (∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
43		df-ral 3143	. . . 4 ⊢ (∀𝑥 ∈ 𝐷 ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
44	5, 42, 43	3bitr4i 305	. . 3 ⊢ (∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥 ∈ 𝐷 ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
45		df-ral 3143	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦(𝑦 ∈ 𝐸 → ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
46		19.21v 1940	. . . . . . . 8 ⊢ (∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ (𝑦 ∈ 𝐸 → ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
47	46	bicomi 226	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐸 → ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
48	47	albii 1820	. . . . . 6 ⊢ (∀𝑦(𝑦 ∈ 𝐸 → ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
49	45, 48	bitri 277	. . . . 5 ⊢ (∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
50	49	bicomi 226	. . . 4 ⊢ (∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
51	50	ralbii 3165	. . 3 ⊢ (∀𝑥 ∈ 𝐷 ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
52	44, 51	bitri 277	. 2 ⊢ (∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
53		df-ral 3143	. . . . 5 ⊢ (∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
54	53	bicomi 226	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
55	54	ralbii 3165	. . 3 ⊢ (∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
56	55	ralbii 3165	. 2 ⊢ (∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
57	1, 52, 56	3bitri 299	1 ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 ∀wal 1535 ∈ wcel 2114 ∀wral 3138 ∩ cin 3935 ⊆ wss 3936 class class class wbr 5066 dom cdm 5555 ran crn 5556 ∘ ccom 5559

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pr 5330

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rab 3147 df-v 3496 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-br 5067 df-opab 5129 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566

This theorem is referenced by: cotr2 14337

W3C validator