Step |
Hyp |
Ref |
Expression |
1 |
|
topontop |
|- ( R e. ( TopOn ` X ) -> R e. Top ) |
2 |
|
topontop |
|- ( S e. ( TopOn ` Y ) -> S e. Top ) |
3 |
|
txtop |
|- ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top ) |
4 |
1 2 3
|
syl2an |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) e. Top ) |
5 |
|
eqid |
|- ran ( u e. R , v e. S |-> ( u X. v ) ) = ran ( u e. R , v e. S |-> ( u X. v ) ) |
6 |
|
eqid |
|- U. R = U. R |
7 |
|
eqid |
|- U. S = U. S |
8 |
5 6 7
|
txuni2 |
|- ( U. R X. U. S ) = U. ran ( u e. R , v e. S |-> ( u X. v ) ) |
9 |
|
toponuni |
|- ( R e. ( TopOn ` X ) -> X = U. R ) |
10 |
|
toponuni |
|- ( S e. ( TopOn ` Y ) -> Y = U. S ) |
11 |
|
xpeq12 |
|- ( ( X = U. R /\ Y = U. S ) -> ( X X. Y ) = ( U. R X. U. S ) ) |
12 |
9 10 11
|
syl2an |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( X X. Y ) = ( U. R X. U. S ) ) |
13 |
5
|
txbasex |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ran ( u e. R , v e. S |-> ( u X. v ) ) e. _V ) |
14 |
|
unitg |
|- ( ran ( u e. R , v e. S |-> ( u X. v ) ) e. _V -> U. ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) = U. ran ( u e. R , v e. S |-> ( u X. v ) ) ) |
15 |
13 14
|
syl |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> U. ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) = U. ran ( u e. R , v e. S |-> ( u X. v ) ) ) |
16 |
8 12 15
|
3eqtr4a |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( X X. Y ) = U. ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) ) |
17 |
5
|
txval |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) = ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) ) |
18 |
17
|
unieqd |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> U. ( R tX S ) = U. ( topGen ` ran ( u e. R , v e. S |-> ( u X. v ) ) ) ) |
19 |
16 18
|
eqtr4d |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( X X. Y ) = U. ( R tX S ) ) |
20 |
|
istopon |
|- ( ( R tX S ) e. ( TopOn ` ( X X. Y ) ) <-> ( ( R tX S ) e. Top /\ ( X X. Y ) = U. ( R tX S ) ) ) |
21 |
4 19 20
|
sylanbrc |
|- ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( R tX S ) e. ( TopOn ` ( X X. Y ) ) ) |