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 } |