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 
|- ( ph -> ( x o. x ) C_ x )
Assertion cotrintab 
|- ( |^| { x | ph } o. |^| { x | ph } ) C_ |^| { x | ph }

Proof

Step Hyp Ref Expression
1 cotrintab.min 
 |-  ( ph -> ( x o. x ) C_ x )
2 cotr 
 |-  ( ( |^| { x | ph } o. |^| { x | ph } ) C_ |^| { x | ph } <-> A. u A. w A. v ( ( u |^| { x | ph } w /\ w |^| { x | ph } v ) -> u |^| { x | ph } v ) )
3 pm3.43 
 |-  ( ( ( ph -> u x w ) /\ ( ph -> w x v ) ) -> ( ph -> ( u x w /\ w x v ) ) )
4 cotr 
 |-  ( ( x o. x ) C_ x <-> A. u A. w A. v ( ( u x w /\ w x v ) -> u x v ) )
5 4 biimpi 
 |-  ( ( x o. x ) C_ x -> A. u A. w A. v ( ( u x w /\ w x v ) -> u x v ) )
6 2sp 
 |-  ( A. w A. v ( ( u x w /\ w x v ) -> u x v ) -> ( ( u x w /\ w x v ) -> u x v ) )
7 6 sps 
 |-  ( A. u A. w A. v ( ( u x w /\ w x v ) -> u x v ) -> ( ( u x w /\ w x v ) -> u x v ) )
8 1 5 7 3syl 
 |-  ( ph -> ( ( u x w /\ w x v ) -> u x v ) )
9 3 8 sylcom 
 |-  ( ( ( ph -> u x w ) /\ ( ph -> w x v ) ) -> ( ph -> u x v ) )
10 9 alanimi 
 |-  ( ( A. x ( ph -> u x w ) /\ A. x ( ph -> w x v ) ) -> A. x ( ph -> u x v ) )
11 opex 
 |-  <. u , w >. e. _V
12 11 elintab 
 |-  ( <. u , w >. e. |^| { x | ph } <-> A. x ( ph -> <. u , w >. e. x ) )
13 df-br 
 |-  ( u |^| { x | ph } w <-> <. u , w >. e. |^| { x | ph } )
14 df-br 
 |-  ( u x w <-> <. u , w >. e. x )
15 14 imbi2i 
 |-  ( ( ph -> u x w ) <-> ( ph -> <. u , w >. e. x ) )
16 15 albii 
 |-  ( A. x ( ph -> u x w ) <-> A. x ( ph -> <. u , w >. e. x ) )
17 12 13 16 3bitr4i 
 |-  ( u |^| { x | ph } w <-> A. x ( ph -> u x w ) )
18 opex 
 |-  <. w , v >. e. _V
19 18 elintab 
 |-  ( <. w , v >. e. |^| { x | ph } <-> A. x ( ph -> <. w , v >. e. x ) )
20 df-br 
 |-  ( w |^| { x | ph } v <-> <. w , v >. e. |^| { x | ph } )
21 df-br 
 |-  ( w x v <-> <. w , v >. e. x )
22 21 imbi2i 
 |-  ( ( ph -> w x v ) <-> ( ph -> <. w , v >. e. x ) )
23 22 albii 
 |-  ( A. x ( ph -> w x v ) <-> A. x ( ph -> <. w , v >. e. x ) )
24 19 20 23 3bitr4i 
 |-  ( w |^| { x | ph } v <-> A. x ( ph -> w x v ) )
25 17 24 anbi12i 
 |-  ( ( u |^| { x | ph } w /\ w |^| { x | ph } v ) <-> ( A. x ( ph -> u x w ) /\ A. x ( ph -> w x v ) ) )
26 opex 
 |-  <. u , v >. e. _V
27 26 elintab 
 |-  ( <. u , v >. e. |^| { x | ph } <-> A. x ( ph -> <. u , v >. e. x ) )
28 df-br 
 |-  ( u |^| { x | ph } v <-> <. u , v >. e. |^| { x | ph } )
29 df-br 
 |-  ( u x v <-> <. u , v >. e. x )
30 29 imbi2i 
 |-  ( ( ph -> u x v ) <-> ( ph -> <. u , v >. e. x ) )
31 30 albii 
 |-  ( A. x ( ph -> u x v ) <-> A. x ( ph -> <. u , v >. e. x ) )
32 27 28 31 3bitr4i 
 |-  ( u |^| { x | ph } v <-> A. x ( ph -> u x v ) )
33 10 25 32 3imtr4i 
 |-  ( ( u |^| { x | ph } w /\ w |^| { x | ph } v ) -> u |^| { x | ph } v )
34 33 gen2 
 |-  A. w A. v ( ( u |^| { x | ph } w /\ w |^| { x | ph } v ) -> u |^| { x | ph } v )
35 2 34 mpgbir 
 |-  ( |^| { x | ph } o. |^| { x | ph } ) C_ |^| { x | ph }