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	$⊢ φ \to x \circ x \subseteq x$
	Assertion	cotrintab	$⊢ ⋂ \{x \| φ\} \circ ⋂ \{x \| φ\} \subseteq ⋂ \{x \| φ\}$

Proof

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

Metamath Proof Explorer

Theorem cotrintab

Proof