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 15039

Description: Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 15040 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 6116	. 2 ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
2		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐷
3		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑧 𝑥 ∈ 𝐷
4	2, 3	19.21-2 2248	. . . . 5 ⊢ (∀𝑦∀𝑧(𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ (𝑥 ∈ 𝐷 → ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
5	4	albii 1852	. . . 4 ⊢ (∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
6		simpl 488	. . . . . . . . . . 11 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐵𝑦)
7		id 23	. . . . . . . . . . 11 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))
8		simpr 490	. . . . . . . . . . 11 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑦𝐴𝑧)
9	6, 7, 8	3jca 1146	. . . . . . . . . 10 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
10		simp2 1155	. . . . . . . . . 10 ⊢ ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) → (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))
11	9, 10	impbii 212	. . . . . . . . 9 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧))
12		cotr2g.d	. . . . . . . . . . . 12 ⊢ dom 𝐵 ⊆ 𝐷
13		vex 3462	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
14		vex 3462	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
15	13, 14	breldm 5903	. . . . . . . . . . . 12 ⊢ (𝑥𝐵𝑦 → 𝑥 ∈ dom 𝐵)
16	12, 15	sselid 3938	. . . . . . . . . . 11 ⊢ (𝑥𝐵𝑦 → 𝑥 ∈ 𝐷)
17	16	pm4.71ri 570	. . . . . . . . . 10 ⊢ (𝑥𝐵𝑦 ↔ (𝑥 ∈ 𝐷 ∧ 𝑥𝐵𝑦))
18		cotr2g.e	. . . . . . . . . . . 12 ⊢ (ran 𝐵 ∩ dom 𝐴) ⊆ 𝐸
19	13, 14	brelrn 5937	. . . . . . . . . . . . 13 ⊢ (𝑥𝐵𝑦 → 𝑦 ∈ ran 𝐵)
20		vex 3462	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
21	14, 20	breldm 5903	. . . . . . . . . . . . 13 ⊢ (𝑦𝐴𝑧 → 𝑦 ∈ dom 𝐴)
22		elin 3924	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (ran 𝐵 ∩ dom 𝐴) ↔ (𝑦 ∈ ran 𝐵 ∧ 𝑦 ∈ dom 𝐴))
23	22	biimpri 231	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ran 𝐵 ∧ 𝑦 ∈ dom 𝐴) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
24	19, 21, 23	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑦 ∈ (ran 𝐵 ∩ dom 𝐴))
25	18, 24	sselid 3938	. . . . . . . . . . 11 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑦 ∈ 𝐸)
26	25	pm4.71ri 570	. . . . . . . . . 10 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ↔ (𝑦 ∈ 𝐸 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
27		cotr2g.f	. . . . . . . . . . . 12 ⊢ ran 𝐴 ⊆ 𝐹
28	14, 20	brelrn 5937	. . . . . . . . . . . 12 ⊢ (𝑦𝐴𝑧 → 𝑧 ∈ ran 𝐴)
29	27, 28	sselid 3938	. . . . . . . . . . 11 ⊢ (𝑦𝐴𝑧 → 𝑧 ∈ 𝐹)
30	29	pm4.71ri 570	. . . . . . . . . 10 ⊢ (𝑦𝐴𝑧 ↔ (𝑧 ∈ 𝐹 ∧ 𝑦𝐴𝑧))
31	17, 26, 30	3anbi123i 1173	. . . . . . . . 9 ⊢ ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑥𝐵𝑦) ∧ (𝑦 ∈ 𝐸 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦𝐴𝑧)))
32		3an6 1475	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑥𝐵𝑦) ∧ (𝑦 ∈ 𝐸 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦𝐴𝑧)) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)))
33	10, 9	impbii 212	. . . . . . . . . . 11 ⊢ ((𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧) ↔ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧))
34	33	anbi2i 635	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ∧ 𝑦𝐴𝑧)) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
35	32, 34	bitri 278	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑥𝐵𝑦) ∧ (𝑦 ∈ 𝐸 ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦𝐴𝑧)) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
36	11, 31, 35	3bitri 300	. . . . . . . 8 ⊢ ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)))
37	36	imbi1i 352	. . . . . . 7 ⊢ (((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) → 𝑥𝐶𝑧))
38		impexp 456	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) ∧ (𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧)) → 𝑥𝐶𝑧) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
39		3impexp 1377	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ∧ 𝑧 ∈ 𝐹) → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ (𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
40	37, 38, 39	3bitri 300	. . . . . 6 ⊢ (((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ (𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
41	40	albii 1852	. . . . 5 ⊢ (∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
42	41	2albii 1853	. . . 4 ⊢ (∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐷 → (𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
43		df-ral 3083	. . . 4 ⊢ (∀𝑥 ∈ 𝐷 ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))))
44	5, 42, 43	3bitr4i 306	. . 3 ⊢ (∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥 ∈ 𝐷 ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
45		df-ral 3083	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦(𝑦 ∈ 𝐸 → ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
46		19.21v 1972	. . . . . . . 8 ⊢ (∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ (𝑦 ∈ 𝐸 → ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
47	46	bicomi 227	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐸 → ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
48	47	albii 1852	. . . . . 6 ⊢ (∀𝑦(𝑦 ∈ 𝐸 → ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
49	45, 48	bitri 278	. . . . 5 ⊢ (∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))))
50	49	bicomi 227	. . . 4 ⊢ (∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
51	50	ralbii 3114	. . 3 ⊢ (∀𝑥 ∈ 𝐷 ∀𝑦∀𝑧(𝑦 ∈ 𝐸 → (𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))) ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
52	44, 51	bitri 278	. 2 ⊢ (∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
53		df-ral 3083	. . . . 5 ⊢ (∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧) ↔ ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)))
54	53	bicomi 227	. . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
55	54	ralbii 3114	. . 3 ⊢ (∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
56	55	ralbii 3114	. 2 ⊢ (∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧(𝑧 ∈ 𝐹 → ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))
57	1, 52, 56	3bitri 300	1 ⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐸 ∀𝑧 ∈ 𝐹 ((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 ∀wal 1568 ∈ wcel 2146 ∀wral 3082 ∩ cin 3907 ⊆ wss 3908 class class class wbr 5114 dom cdm 5666 ran crn 5667 ∘ ccom 5670

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-pr 5409

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-clab 2745 df-cleq 2758 df-clel 2841 df-ral 3083 df-rab 3420 df-v 3460 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-br 5115 df-opab 5179 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677

This theorem is used by: cotr2 15040

W3C validator