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