Metamath Proof Explorer

Theorem txcn

Description: A map into the product of two topological spaces is continuous iff both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses txcn.1 
|- X = U. R
txcn.2 
|- Y = U. S
txcn.3 
|- Z = ( X X. Y )
txcn.4 
|- W = U. U
txcn.5 
|- P = ( 1st |` Z )
txcn.6 
|- Q = ( 2nd |` Z )
Assertion txcn 
|- ( ( R e. Top /\ S e. Top /\ F : W --> Z ) -> ( F e. ( U Cn ( R tX S ) ) <-> ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) )

Proof

Step Hyp Ref Expression
1 txcn.1 
 |-  X = U. R
2 txcn.2 
 |-  Y = U. S
3 txcn.3 
 |-  Z = ( X X. Y )
4 txcn.4 
 |-  W = U. U
5 txcn.5 
 |-  P = ( 1st |` Z )
6 txcn.6 
 |-  Q = ( 2nd |` Z )
7 1 toptopon 
 |-  ( R e. Top <-> R e. ( TopOn ` X ) )
8 2 toptopon 
 |-  ( S e. Top <-> S e. ( TopOn ` Y ) )
9 3 reseq2i 
 |-  ( 1st |` Z ) = ( 1st |` ( X X. Y ) )
10 5 9 eqtri 
 |-  P = ( 1st |` ( X X. Y ) )
11 tx1cn 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) )
12 10 11 eqeltrid 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> P e. ( ( R tX S ) Cn R ) )
13 3 reseq2i 
 |-  ( 2nd |` Z ) = ( 2nd |` ( X X. Y ) )
14 6 13 eqtri 
 |-  Q = ( 2nd |` ( X X. Y ) )
15 tx2cn 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) )
16 14 15 eqeltrid 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> Q e. ( ( R tX S ) Cn S ) )
17 cnco 
 |-  ( ( F e. ( U Cn ( R tX S ) ) /\ P e. ( ( R tX S ) Cn R ) ) -> ( P o. F ) e. ( U Cn R ) )
18 cnco 
 |-  ( ( F e. ( U Cn ( R tX S ) ) /\ Q e. ( ( R tX S ) Cn S ) ) -> ( Q o. F ) e. ( U Cn S ) )
19 17 18 anim12dan 
 |-  ( ( F e. ( U Cn ( R tX S ) ) /\ ( P e. ( ( R tX S ) Cn R ) /\ Q e. ( ( R tX S ) Cn S ) ) ) -> ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) )
20 19 expcom 
 |-  ( ( P e. ( ( R tX S ) Cn R ) /\ Q e. ( ( R tX S ) Cn S ) ) -> ( F e. ( U Cn ( R tX S ) ) -> ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) )
21 12 16 20 syl2anc 
 |-  ( ( R e. ( TopOn ` X ) /\ S e. ( TopOn ` Y ) ) -> ( F e. ( U Cn ( R tX S ) ) -> ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) )
22 7 8 21 syl2anb 
 |-  ( ( R e. Top /\ S e. Top ) -> ( F e. ( U Cn ( R tX S ) ) -> ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) )
23 22 3adant3 
 |-  ( ( R e. Top /\ S e. Top /\ F : W --> Z ) -> ( F e. ( U Cn ( R tX S ) ) -> ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) )
24 cntop1 
 |-  ( ( P o. F ) e. ( U Cn R ) -> U e. Top )
25 24 ad2antrl 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> U e. Top )
26 4 topopn 
 |-  ( U e. Top -> W e. U )
27 25 26 syl 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> W e. U )
28 4 1 cnf 
 |-  ( ( P o. F ) e. ( U Cn R ) -> ( P o. F ) : W --> X )
29 28 ad2antrl 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> ( P o. F ) : W --> X )
30 4 2 cnf 
 |-  ( ( Q o. F ) e. ( U Cn S ) -> ( Q o. F ) : W --> Y )
31 30 ad2antll 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> ( Q o. F ) : W --> Y )
32 10 14 upxp 
 |-  ( ( W e. U /\ ( P o. F ) : W --> X /\ ( Q o. F ) : W --> Y ) -> E! h ( h : W --> ( X X. Y ) /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
33 feq3 
 |-  ( Z = ( X X. Y ) -> ( h : W --> Z <-> h : W --> ( X X. Y ) ) )
34 3 33 ax-mp 
 |-  ( h : W --> Z <-> h : W --> ( X X. Y ) )
35 34 3anbi1i 
 |-  ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) <-> ( h : W --> ( X X. Y ) /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
36 35 eubii 
 |-  ( E! h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) <-> E! h ( h : W --> ( X X. Y ) /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
37 32 36 sylibr 
 |-  ( ( W e. U /\ ( P o. F ) : W --> X /\ ( Q o. F ) : W --> Y ) -> E! h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
38 27 29 31 37 syl3anc 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> E! h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
39 euex 
 |-  ( E! h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) -> E. h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
40 38 39 syl 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> E. h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
41 simpll3 
 |-  ( ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) /\ ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> F : W --> Z )
42 27 adantr 
 |-  ( ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) /\ ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> W e. U )
43 1 topopn 
 |-  ( R e. Top -> X e. R )
44 2 topopn 
 |-  ( S e. Top -> Y e. S )
45 xpexg 
 |-  ( ( X e. R /\ Y e. S ) -> ( X X. Y ) e. _V )
46 3 45 eqeltrid 
 |-  ( ( X e. R /\ Y e. S ) -> Z e. _V )
47 43 44 46 syl2an 
 |-  ( ( R e. Top /\ S e. Top ) -> Z e. _V )
48 47 3adant3 
 |-  ( ( R e. Top /\ S e. Top /\ F : W --> Z ) -> Z e. _V )
49 48 ad2antrr 
 |-  ( ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) /\ ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> Z e. _V )
50 fex2 
 |-  ( ( F : W --> Z /\ W e. U /\ Z e. _V ) -> F e. _V )
51 41 42 49 50 syl3anc 
 |-  ( ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) /\ ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> F e. _V )
52 eumo 
 |-  ( E! h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) -> E* h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
53 38 52 syl 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> E* h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
54 53 adantr 
 |-  ( ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) /\ ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> E* h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
55 simpr 
 |-  ( ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) /\ ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
56 3anass 
 |-  ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) <-> ( h : W --> Z /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) )
57 coeq2 
 |-  ( F = h -> ( P o. F ) = ( P o. h ) )
58 coeq2 
 |-  ( F = h -> ( Q o. F ) = ( Q o. h ) )
59 57 58 jca 
 |-  ( F = h -> ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
60 59 eqcoms 
 |-  ( h = F -> ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
61 60 biantrud 
 |-  ( h = F -> ( h : W --> Z <-> ( h : W --> Z /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) ) )
62 feq1 
 |-  ( h = F -> ( h : W --> Z <-> F : W --> Z ) )
63 61 62 bitr3d 
 |-  ( h = F -> ( ( h : W --> Z /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) <-> F : W --> Z ) )
64 56 63 syl5bb 
 |-  ( h = F -> ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) <-> F : W --> Z ) )
65 64 moi2 
 |-  ( ( ( F e. _V /\ E* h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) /\ ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) /\ F : W --> Z ) ) -> h = F )
66 51 54 55 41 65 syl22anc 
 |-  ( ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) /\ ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> h = F )
67 eqid 
 |-  ( R tX S ) = ( R tX S )
68 67 1 2 3 5 6 uptx 
 |-  ( ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) -> E! h e. ( U Cn ( R tX S ) ) ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
69 68 adantl 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> E! h e. ( U Cn ( R tX S ) ) ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) )
70 df-reu 
 |-  ( E! h e. ( U Cn ( R tX S ) ) ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) <-> E! h ( h e. ( U Cn ( R tX S ) ) /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) )
71 euex 
 |-  ( E! h ( h e. ( U Cn ( R tX S ) ) /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> E. h ( h e. ( U Cn ( R tX S ) ) /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) )
72 70 71 sylbi 
 |-  ( E! h e. ( U Cn ( R tX S ) ) ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) -> E. h ( h e. ( U Cn ( R tX S ) ) /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) )
73 eqid 
 |-  U. ( R tX S ) = U. ( R tX S )
74 4 73 cnf 
 |-  ( h e. ( U Cn ( R tX S ) ) -> h : W --> U. ( R tX S ) )
75 1 2 txuni 
 |-  ( ( R e. Top /\ S e. Top ) -> ( X X. Y ) = U. ( R tX S ) )
76 3 75 syl5eq 
 |-  ( ( R e. Top /\ S e. Top ) -> Z = U. ( R tX S ) )
77 76 3adant3 
 |-  ( ( R e. Top /\ S e. Top /\ F : W --> Z ) -> Z = U. ( R tX S ) )
78 77 adantr 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> Z = U. ( R tX S ) )
79 78 feq3d 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> ( h : W --> Z <-> h : W --> U. ( R tX S ) ) )
80 74 79 syl5ibr 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> ( h e. ( U Cn ( R tX S ) ) -> h : W --> Z ) )
81 80 anim1d 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> ( ( h e. ( U Cn ( R tX S ) ) /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> ( h : W --> Z /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) ) )
82 81 56 syl6ibr 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> ( ( h e. ( U Cn ( R tX S ) ) /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) )
83 simpl 
 |-  ( ( h e. ( U Cn ( R tX S ) ) /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> h e. ( U Cn ( R tX S ) ) )
84 82 83 jca2 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> ( ( h e. ( U Cn ( R tX S ) ) /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) /\ h e. ( U Cn ( R tX S ) ) ) ) )
85 84 eximdv 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> ( E. h ( h e. ( U Cn ( R tX S ) ) /\ ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> E. h ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) /\ h e. ( U Cn ( R tX S ) ) ) ) )
86 72 85 syl5 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> ( E! h e. ( U Cn ( R tX S ) ) ( ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) -> E. h ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) /\ h e. ( U Cn ( R tX S ) ) ) ) )
87 69 86 mpd 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> E. h ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) /\ h e. ( U Cn ( R tX S ) ) ) )
88 eupick 
 |-  ( ( E! h ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) /\ E. h ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) /\ h e. ( U Cn ( R tX S ) ) ) ) -> ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) -> h e. ( U Cn ( R tX S ) ) ) )
89 38 87 88 syl2anc 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> ( ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) -> h e. ( U Cn ( R tX S ) ) ) )
90 89 imp 
 |-  ( ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) /\ ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> h e. ( U Cn ( R tX S ) ) )
91 66 90 eqeltrrd 
 |-  ( ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) /\ ( h : W --> Z /\ ( P o. F ) = ( P o. h ) /\ ( Q o. F ) = ( Q o. h ) ) ) -> F e. ( U Cn ( R tX S ) ) )
92 40 91 exlimddv 
 |-  ( ( ( R e. Top /\ S e. Top /\ F : W --> Z ) /\ ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) -> F e. ( U Cn ( R tX S ) ) )
93 92 ex 
 |-  ( ( R e. Top /\ S e. Top /\ F : W --> Z ) -> ( ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) -> F e. ( U Cn ( R tX S ) ) ) )
94 23 93 impbid 
 |-  ( ( R e. Top /\ S e. Top /\ F : W --> Z ) -> ( F e. ( U Cn ( R tX S ) ) <-> ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) )