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 ⊢ φ → x ∘ x ⊆ x
Assertion cotrintab ⊢ ⋂ x | φ ∘ ⋂ x | φ ⊆ ⋂ x | φ

Proof

Step Hyp Ref Expression
1 cotrintab.min ⊢ φ → x ∘ x ⊆ x
2 cotr ⊢ ⋂ x | φ ∘ ⋂ x | φ ⊆ ⋂ x | φ ↔ ∀ u ∀ w ∀ v u ⋂ x | φ w ∧ w ⋂ x | φ v → u ⋂ x | φ v
3 pm3.43 ⊢ φ → u x w ∧ φ → w x v → φ → u x w ∧ w x v
4 cotr ⊢ x ∘ x ⊆ x ↔ ∀ u ∀ w ∀ v u x w ∧ w x v → u x v
5 4 biimpi ⊢ x ∘ x ⊆ x → ∀ u ∀ w ∀ v u x w ∧ w x v → u x v
6 2sp ⊢ ∀ w ∀ v u x w ∧ w x v → u x v → u x w ∧ w x v → u x v
7 6 sps ⊢ ∀ u ∀ w ∀ v u x w ∧ w x v → u x v → u x w ∧ w x v → u x v
8 1 5 7 3syl ⊢ φ → u x w ∧ w x v → u x v
9 3 8 sylcom ⊢ φ → u x w ∧ φ → w x v → φ → u x v
10 9 alanimi ⊢ ∀ x φ → u x w ∧ ∀ x φ → w x v → ∀ x φ → u x v
11 opex ⊢ u w ∈ V
12 11 elintab ⊢ u w ∈ ⋂ x | φ ↔ ∀ x φ → u w ∈ x
13 df-br ⊢ u ⋂ x | φ w ↔ u w ∈ ⋂ x | φ
14 df-br ⊢ u x w ↔ u w ∈ x
15 14 imbi2i ⊢ φ → u x w ↔ φ → u w ∈ x
16 15 albii ⊢ ∀ x φ → u x w ↔ ∀ x φ → u w ∈ x
17 12 13 16 3bitr4i ⊢ u ⋂ x | φ w ↔ ∀ x φ → u x w
18 opex ⊢ w v ∈ V
19 18 elintab ⊢ w v ∈ ⋂ x | φ ↔ ∀ x φ → w v ∈ x
20 df-br ⊢ w ⋂ x | φ v ↔ w v ∈ ⋂ x | φ
21 df-br ⊢ w x v ↔ w v ∈ x
22 21 imbi2i ⊢ φ → w x v ↔ φ → w v ∈ x
23 22 albii ⊢ ∀ x φ → w x v ↔ ∀ x φ → w v ∈ x
24 19 20 23 3bitr4i ⊢ w ⋂ x | φ v ↔ ∀ x φ → w x v
25 17 24 anbi12i ⊢ u ⋂ x | φ w ∧ w ⋂ x | φ v ↔ ∀ x φ → u x w ∧ ∀ x φ → w x v
26 opex ⊢ u v ∈ V
27 26 elintab ⊢ u v ∈ ⋂ x | φ ↔ ∀ x φ → u v ∈ x
28 df-br ⊢ u ⋂ x | φ v ↔ u v ∈ ⋂ x | φ
29 df-br ⊢ u x v ↔ u v ∈ x
30 29 imbi2i ⊢ φ → u x v ↔ φ → u v ∈ x
31 30 albii ⊢ ∀ x φ → u x v ↔ ∀ x φ → u v ∈ x
32 27 28 31 3bitr4i ⊢ u ⋂ x | φ v ↔ ∀ x φ → u x v
33 10 25 32 3imtr4i ⊢ u ⋂ x | φ w ∧ w ⋂ x | φ v → u ⋂ x | φ v
34 33 gen2 ⊢ ∀ w ∀ v u ⋂ x | φ w ∧ w ⋂ x | φ v → u ⋂ x | φ v
35 2 34 mpgbir ⊢ ⋂ x | φ ∘ ⋂ x | φ ⊆ ⋂ x | φ