Step |
Hyp |
Ref |
Expression |
1 |
|
neitx.x |
|- X = U. J |
2 |
|
neitx.y |
|- Y = U. K |
3 |
1
|
neii1 |
|- ( ( J e. Top /\ A e. ( ( nei ` J ) ` C ) ) -> A C_ X ) |
4 |
3
|
ad2ant2r |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> A C_ X ) |
5 |
2
|
neii1 |
|- ( ( K e. Top /\ B e. ( ( nei ` K ) ` D ) ) -> B C_ Y ) |
6 |
5
|
ad2ant2l |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> B C_ Y ) |
7 |
|
xpss12 |
|- ( ( A C_ X /\ B C_ Y ) -> ( A X. B ) C_ ( X X. Y ) ) |
8 |
4 6 7
|
syl2anc |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( A X. B ) C_ ( X X. Y ) ) |
9 |
1 2
|
txuni |
|- ( ( J e. Top /\ K e. Top ) -> ( X X. Y ) = U. ( J tX K ) ) |
10 |
9
|
adantr |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( X X. Y ) = U. ( J tX K ) ) |
11 |
8 10
|
sseqtrd |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( A X. B ) C_ U. ( J tX K ) ) |
12 |
|
simp-5l |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> ( J e. Top /\ K e. Top ) ) |
13 |
|
simp-4r |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> a e. J ) |
14 |
|
simplr |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> b e. K ) |
15 |
|
txopn |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( a e. J /\ b e. K ) ) -> ( a X. b ) e. ( J tX K ) ) |
16 |
12 13 14 15
|
syl12anc |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> ( a X. b ) e. ( J tX K ) ) |
17 |
|
simpr1l |
|- ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( ( C C_ a /\ a C_ A ) /\ b e. K /\ ( D C_ b /\ b C_ B ) ) ) -> C C_ a ) |
18 |
17
|
3anassrs |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> C C_ a ) |
19 |
|
simprl |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> D C_ b ) |
20 |
|
xpss12 |
|- ( ( C C_ a /\ D C_ b ) -> ( C X. D ) C_ ( a X. b ) ) |
21 |
18 19 20
|
syl2anc |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> ( C X. D ) C_ ( a X. b ) ) |
22 |
|
simpr1r |
|- ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( ( C C_ a /\ a C_ A ) /\ b e. K /\ ( D C_ b /\ b C_ B ) ) ) -> a C_ A ) |
23 |
22
|
3anassrs |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> a C_ A ) |
24 |
|
simprr |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> b C_ B ) |
25 |
|
xpss12 |
|- ( ( a C_ A /\ b C_ B ) -> ( a X. b ) C_ ( A X. B ) ) |
26 |
23 24 25
|
syl2anc |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> ( a X. b ) C_ ( A X. B ) ) |
27 |
|
sseq2 |
|- ( c = ( a X. b ) -> ( ( C X. D ) C_ c <-> ( C X. D ) C_ ( a X. b ) ) ) |
28 |
|
sseq1 |
|- ( c = ( a X. b ) -> ( c C_ ( A X. B ) <-> ( a X. b ) C_ ( A X. B ) ) ) |
29 |
27 28
|
anbi12d |
|- ( c = ( a X. b ) -> ( ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) <-> ( ( C X. D ) C_ ( a X. b ) /\ ( a X. b ) C_ ( A X. B ) ) ) ) |
30 |
29
|
rspcev |
|- ( ( ( a X. b ) e. ( J tX K ) /\ ( ( C X. D ) C_ ( a X. b ) /\ ( a X. b ) C_ ( A X. B ) ) ) -> E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) ) |
31 |
16 21 26 30
|
syl12anc |
|- ( ( ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) /\ b e. K ) /\ ( D C_ b /\ b C_ B ) ) -> E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) ) |
32 |
|
neii2 |
|- ( ( K e. Top /\ B e. ( ( nei ` K ) ` D ) ) -> E. b e. K ( D C_ b /\ b C_ B ) ) |
33 |
32
|
ad2ant2l |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> E. b e. K ( D C_ b /\ b C_ B ) ) |
34 |
33
|
ad2antrr |
|- ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) -> E. b e. K ( D C_ b /\ b C_ B ) ) |
35 |
31 34
|
r19.29a |
|- ( ( ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) /\ a e. J ) /\ ( C C_ a /\ a C_ A ) ) -> E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) ) |
36 |
|
neii2 |
|- ( ( J e. Top /\ A e. ( ( nei ` J ) ` C ) ) -> E. a e. J ( C C_ a /\ a C_ A ) ) |
37 |
36
|
ad2ant2r |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> E. a e. J ( C C_ a /\ a C_ A ) ) |
38 |
35 37
|
r19.29a |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) ) |
39 |
|
txtop |
|- ( ( J e. Top /\ K e. Top ) -> ( J tX K ) e. Top ) |
40 |
39
|
adantr |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( J tX K ) e. Top ) |
41 |
1
|
neiss2 |
|- ( ( J e. Top /\ A e. ( ( nei ` J ) ` C ) ) -> C C_ X ) |
42 |
41
|
ad2ant2r |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> C C_ X ) |
43 |
2
|
neiss2 |
|- ( ( K e. Top /\ B e. ( ( nei ` K ) ` D ) ) -> D C_ Y ) |
44 |
43
|
ad2ant2l |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> D C_ Y ) |
45 |
|
xpss12 |
|- ( ( C C_ X /\ D C_ Y ) -> ( C X. D ) C_ ( X X. Y ) ) |
46 |
42 44 45
|
syl2anc |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( C X. D ) C_ ( X X. Y ) ) |
47 |
46 10
|
sseqtrd |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( C X. D ) C_ U. ( J tX K ) ) |
48 |
|
eqid |
|- U. ( J tX K ) = U. ( J tX K ) |
49 |
48
|
isnei |
|- ( ( ( J tX K ) e. Top /\ ( C X. D ) C_ U. ( J tX K ) ) -> ( ( A X. B ) e. ( ( nei ` ( J tX K ) ) ` ( C X. D ) ) <-> ( ( A X. B ) C_ U. ( J tX K ) /\ E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) ) ) ) |
50 |
40 47 49
|
syl2anc |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( ( A X. B ) e. ( ( nei ` ( J tX K ) ) ` ( C X. D ) ) <-> ( ( A X. B ) C_ U. ( J tX K ) /\ E. c e. ( J tX K ) ( ( C X. D ) C_ c /\ c C_ ( A X. B ) ) ) ) ) |
51 |
11 38 50
|
mpbir2and |
|- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( A X. B ) e. ( ( nei ` ( J tX K ) ) ` ( C X. D ) ) ) |