Step |
Hyp |
Ref |
Expression |
1 |
|
elxp2 |
|- ( z e. ( T X. T ) <-> E. x e. T E. y e. T z = <. x , y >. ) |
2 |
|
tskop |
|- ( ( T e. Tarski /\ x e. T /\ y e. T ) -> <. x , y >. e. T ) |
3 |
|
eleq1a |
|- ( <. x , y >. e. T -> ( z = <. x , y >. -> z e. T ) ) |
4 |
2 3
|
syl |
|- ( ( T e. Tarski /\ x e. T /\ y e. T ) -> ( z = <. x , y >. -> z e. T ) ) |
5 |
4
|
3expib |
|- ( T e. Tarski -> ( ( x e. T /\ y e. T ) -> ( z = <. x , y >. -> z e. T ) ) ) |
6 |
5
|
rexlimdvv |
|- ( T e. Tarski -> ( E. x e. T E. y e. T z = <. x , y >. -> z e. T ) ) |
7 |
1 6
|
syl5bi |
|- ( T e. Tarski -> ( z e. ( T X. T ) -> z e. T ) ) |
8 |
7
|
ssrdv |
|- ( T e. Tarski -> ( T X. T ) C_ T ) |
9 |
|
xpss12 |
|- ( ( A C_ T /\ B C_ T ) -> ( A X. B ) C_ ( T X. T ) ) |
10 |
|
sstr |
|- ( ( ( A X. B ) C_ ( T X. T ) /\ ( T X. T ) C_ T ) -> ( A X. B ) C_ T ) |
11 |
10
|
expcom |
|- ( ( T X. T ) C_ T -> ( ( A X. B ) C_ ( T X. T ) -> ( A X. B ) C_ T ) ) |
12 |
8 9 11
|
syl2im |
|- ( T e. Tarski -> ( ( A C_ T /\ B C_ T ) -> ( A X. B ) C_ T ) ) |
13 |
12
|
3impib |
|- ( ( T e. Tarski /\ A C_ T /\ B C_ T ) -> ( A X. B ) C_ T ) |