# Metamath Proof Explorer

## Theorem cotrintab

Description: The intersection of a class is a transitive relation if membership in the class implies the member is a transitive relation. (Contributed by RP, 28-Oct-2020)

Ref Expression
Hypothesis cotrintab.min ${⊢}{\phi }\to {x}\circ {x}\subseteq {x}$
Assertion cotrintab ${⊢}\bigcap \left\{{x}|{\phi }\right\}\circ \bigcap \left\{{x}|{\phi }\right\}\subseteq \bigcap \left\{{x}|{\phi }\right\}$

### Proof

Step Hyp Ref Expression
1 cotrintab.min ${⊢}{\phi }\to {x}\circ {x}\subseteq {x}$
2 cotr ${⊢}\bigcap \left\{{x}|{\phi }\right\}\circ \bigcap \left\{{x}|{\phi }\right\}\subseteq \bigcap \left\{{x}|{\phi }\right\}↔\forall {u}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left(\left({u}\bigcap \left\{{x}|{\phi }\right\}{w}\wedge {w}\bigcap \left\{{x}|{\phi }\right\}{v}\right)\to {u}\bigcap \left\{{x}|{\phi }\right\}{v}\right)$
3 pm3.43 ${⊢}\left(\left({\phi }\to {u}{x}{w}\right)\wedge \left({\phi }\to {w}{x}{v}\right)\right)\to \left({\phi }\to \left({u}{x}{w}\wedge {w}{x}{v}\right)\right)$
4 cotr ${⊢}{x}\circ {x}\subseteq {x}↔\forall {u}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left(\left({u}{x}{w}\wedge {w}{x}{v}\right)\to {u}{x}{v}\right)$
5 4 biimpi ${⊢}{x}\circ {x}\subseteq {x}\to \forall {u}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left(\left({u}{x}{w}\wedge {w}{x}{v}\right)\to {u}{x}{v}\right)$
6 2sp ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left(\left({u}{x}{w}\wedge {w}{x}{v}\right)\to {u}{x}{v}\right)\to \left(\left({u}{x}{w}\wedge {w}{x}{v}\right)\to {u}{x}{v}\right)$
7 6 sps ${⊢}\forall {u}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left(\left({u}{x}{w}\wedge {w}{x}{v}\right)\to {u}{x}{v}\right)\to \left(\left({u}{x}{w}\wedge {w}{x}{v}\right)\to {u}{x}{v}\right)$
8 1 5 7 3syl ${⊢}{\phi }\to \left(\left({u}{x}{w}\wedge {w}{x}{v}\right)\to {u}{x}{v}\right)$
9 3 8 sylcom ${⊢}\left(\left({\phi }\to {u}{x}{w}\right)\wedge \left({\phi }\to {w}{x}{v}\right)\right)\to \left({\phi }\to {u}{x}{v}\right)$
10 9 alanimi ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {u}{x}{w}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {w}{x}{v}\right)\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {u}{x}{v}\right)$
11 opex ${⊢}⟨{u},{w}⟩\in \mathrm{V}$
12 11 elintab ${⊢}⟨{u},{w}⟩\in \bigcap \left\{{x}|{\phi }\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to ⟨{u},{w}⟩\in {x}\right)$
13 df-br ${⊢}{u}\bigcap \left\{{x}|{\phi }\right\}{w}↔⟨{u},{w}⟩\in \bigcap \left\{{x}|{\phi }\right\}$
14 df-br ${⊢}{u}{x}{w}↔⟨{u},{w}⟩\in {x}$
15 14 imbi2i ${⊢}\left({\phi }\to {u}{x}{w}\right)↔\left({\phi }\to ⟨{u},{w}⟩\in {x}\right)$
16 15 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {u}{x}{w}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to ⟨{u},{w}⟩\in {x}\right)$
17 12 13 16 3bitr4i ${⊢}{u}\bigcap \left\{{x}|{\phi }\right\}{w}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {u}{x}{w}\right)$
18 opex ${⊢}⟨{w},{v}⟩\in \mathrm{V}$
19 18 elintab ${⊢}⟨{w},{v}⟩\in \bigcap \left\{{x}|{\phi }\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to ⟨{w},{v}⟩\in {x}\right)$
20 df-br ${⊢}{w}\bigcap \left\{{x}|{\phi }\right\}{v}↔⟨{w},{v}⟩\in \bigcap \left\{{x}|{\phi }\right\}$
21 df-br ${⊢}{w}{x}{v}↔⟨{w},{v}⟩\in {x}$
22 21 imbi2i ${⊢}\left({\phi }\to {w}{x}{v}\right)↔\left({\phi }\to ⟨{w},{v}⟩\in {x}\right)$
23 22 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {w}{x}{v}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to ⟨{w},{v}⟩\in {x}\right)$
24 19 20 23 3bitr4i ${⊢}{w}\bigcap \left\{{x}|{\phi }\right\}{v}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {w}{x}{v}\right)$
25 17 24 anbi12i ${⊢}\left({u}\bigcap \left\{{x}|{\phi }\right\}{w}\wedge {w}\bigcap \left\{{x}|{\phi }\right\}{v}\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {u}{x}{w}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {w}{x}{v}\right)\right)$
26 opex ${⊢}⟨{u},{v}⟩\in \mathrm{V}$
27 26 elintab ${⊢}⟨{u},{v}⟩\in \bigcap \left\{{x}|{\phi }\right\}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to ⟨{u},{v}⟩\in {x}\right)$
28 df-br ${⊢}{u}\bigcap \left\{{x}|{\phi }\right\}{v}↔⟨{u},{v}⟩\in \bigcap \left\{{x}|{\phi }\right\}$
29 df-br ${⊢}{u}{x}{v}↔⟨{u},{v}⟩\in {x}$
30 29 imbi2i ${⊢}\left({\phi }\to {u}{x}{v}\right)↔\left({\phi }\to ⟨{u},{v}⟩\in {x}\right)$
31 30 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {u}{x}{v}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to ⟨{u},{v}⟩\in {x}\right)$
32 27 28 31 3bitr4i ${⊢}{u}\bigcap \left\{{x}|{\phi }\right\}{v}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {u}{x}{v}\right)$
33 10 25 32 3imtr4i ${⊢}\left({u}\bigcap \left\{{x}|{\phi }\right\}{w}\wedge {w}\bigcap \left\{{x}|{\phi }\right\}{v}\right)\to {u}\bigcap \left\{{x}|{\phi }\right\}{v}$
34 33 gen2 ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\forall {v}\phantom{\rule{.4em}{0ex}}\left(\left({u}\bigcap \left\{{x}|{\phi }\right\}{w}\wedge {w}\bigcap \left\{{x}|{\phi }\right\}{v}\right)\to {u}\bigcap \left\{{x}|{\phi }\right\}{v}\right)$
35 2 34 mpgbir ${⊢}\bigcap \left\{{x}|{\phi }\right\}\circ \bigcap \left\{{x}|{\phi }\right\}\subseteq \bigcap \left\{{x}|{\phi }\right\}$