Step |
Hyp |
Ref |
Expression |
1 |
|
uncmp.1 |
|- X = U. J |
2 |
|
simpll |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> J e. Top ) |
3 |
|
simpll |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> J e. Top ) |
4 |
|
ssun1 |
|- S C_ ( S u. T ) |
5 |
|
sseq2 |
|- ( X = ( S u. T ) -> ( S C_ X <-> S C_ ( S u. T ) ) ) |
6 |
4 5
|
mpbiri |
|- ( X = ( S u. T ) -> S C_ X ) |
7 |
6
|
ad2antlr |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> S C_ X ) |
8 |
1
|
cmpsub |
|- ( ( J e. Top /\ S C_ X ) -> ( ( J |`t S ) e. Comp <-> A. m e. ~P J ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) ) ) |
9 |
3 7 8
|
syl2anc |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( J |`t S ) e. Comp <-> A. m e. ~P J ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) ) ) |
10 |
|
simprr |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> X = U. c ) |
11 |
7 10
|
sseqtrd |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> S C_ U. c ) |
12 |
|
unieq |
|- ( m = c -> U. m = U. c ) |
13 |
12
|
sseq2d |
|- ( m = c -> ( S C_ U. m <-> S C_ U. c ) ) |
14 |
|
pweq |
|- ( m = c -> ~P m = ~P c ) |
15 |
14
|
ineq1d |
|- ( m = c -> ( ~P m i^i Fin ) = ( ~P c i^i Fin ) ) |
16 |
15
|
rexeqdv |
|- ( m = c -> ( E. n e. ( ~P m i^i Fin ) S C_ U. n <-> E. n e. ( ~P c i^i Fin ) S C_ U. n ) ) |
17 |
13 16
|
imbi12d |
|- ( m = c -> ( ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) <-> ( S C_ U. c -> E. n e. ( ~P c i^i Fin ) S C_ U. n ) ) ) |
18 |
17
|
rspcv |
|- ( c e. ~P J -> ( A. m e. ~P J ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) -> ( S C_ U. c -> E. n e. ( ~P c i^i Fin ) S C_ U. n ) ) ) |
19 |
18
|
ad2antrl |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( A. m e. ~P J ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) -> ( S C_ U. c -> E. n e. ( ~P c i^i Fin ) S C_ U. n ) ) ) |
20 |
11 19
|
mpid |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( A. m e. ~P J ( S C_ U. m -> E. n e. ( ~P m i^i Fin ) S C_ U. n ) -> E. n e. ( ~P c i^i Fin ) S C_ U. n ) ) |
21 |
9 20
|
sylbid |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( J |`t S ) e. Comp -> E. n e. ( ~P c i^i Fin ) S C_ U. n ) ) |
22 |
|
ssun2 |
|- T C_ ( S u. T ) |
23 |
|
sseq2 |
|- ( X = ( S u. T ) -> ( T C_ X <-> T C_ ( S u. T ) ) ) |
24 |
22 23
|
mpbiri |
|- ( X = ( S u. T ) -> T C_ X ) |
25 |
24
|
ad2antlr |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> T C_ X ) |
26 |
1
|
cmpsub |
|- ( ( J e. Top /\ T C_ X ) -> ( ( J |`t T ) e. Comp <-> A. r e. ~P J ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) ) ) |
27 |
3 25 26
|
syl2anc |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( J |`t T ) e. Comp <-> A. r e. ~P J ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) ) ) |
28 |
25 10
|
sseqtrd |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> T C_ U. c ) |
29 |
|
unieq |
|- ( r = c -> U. r = U. c ) |
30 |
29
|
sseq2d |
|- ( r = c -> ( T C_ U. r <-> T C_ U. c ) ) |
31 |
|
pweq |
|- ( r = c -> ~P r = ~P c ) |
32 |
31
|
ineq1d |
|- ( r = c -> ( ~P r i^i Fin ) = ( ~P c i^i Fin ) ) |
33 |
32
|
rexeqdv |
|- ( r = c -> ( E. s e. ( ~P r i^i Fin ) T C_ U. s <-> E. s e. ( ~P c i^i Fin ) T C_ U. s ) ) |
34 |
30 33
|
imbi12d |
|- ( r = c -> ( ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) <-> ( T C_ U. c -> E. s e. ( ~P c i^i Fin ) T C_ U. s ) ) ) |
35 |
34
|
rspcv |
|- ( c e. ~P J -> ( A. r e. ~P J ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) -> ( T C_ U. c -> E. s e. ( ~P c i^i Fin ) T C_ U. s ) ) ) |
36 |
35
|
ad2antrl |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( A. r e. ~P J ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) -> ( T C_ U. c -> E. s e. ( ~P c i^i Fin ) T C_ U. s ) ) ) |
37 |
28 36
|
mpid |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( A. r e. ~P J ( T C_ U. r -> E. s e. ( ~P r i^i Fin ) T C_ U. s ) -> E. s e. ( ~P c i^i Fin ) T C_ U. s ) ) |
38 |
27 37
|
sylbid |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( J |`t T ) e. Comp -> E. s e. ( ~P c i^i Fin ) T C_ U. s ) ) |
39 |
|
reeanv |
|- ( E. n e. ( ~P c i^i Fin ) E. s e. ( ~P c i^i Fin ) ( S C_ U. n /\ T C_ U. s ) <-> ( E. n e. ( ~P c i^i Fin ) S C_ U. n /\ E. s e. ( ~P c i^i Fin ) T C_ U. s ) ) |
40 |
|
elinel1 |
|- ( n e. ( ~P c i^i Fin ) -> n e. ~P c ) |
41 |
40
|
elpwid |
|- ( n e. ( ~P c i^i Fin ) -> n C_ c ) |
42 |
|
elinel1 |
|- ( s e. ( ~P c i^i Fin ) -> s e. ~P c ) |
43 |
42
|
elpwid |
|- ( s e. ( ~P c i^i Fin ) -> s C_ c ) |
44 |
41 43
|
anim12i |
|- ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) -> ( n C_ c /\ s C_ c ) ) |
45 |
44
|
ad2antrl |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( n C_ c /\ s C_ c ) ) |
46 |
|
unss |
|- ( ( n C_ c /\ s C_ c ) <-> ( n u. s ) C_ c ) |
47 |
45 46
|
sylib |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( n u. s ) C_ c ) |
48 |
|
elinel2 |
|- ( n e. ( ~P c i^i Fin ) -> n e. Fin ) |
49 |
|
elinel2 |
|- ( s e. ( ~P c i^i Fin ) -> s e. Fin ) |
50 |
|
unfi |
|- ( ( n e. Fin /\ s e. Fin ) -> ( n u. s ) e. Fin ) |
51 |
48 49 50
|
syl2an |
|- ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) -> ( n u. s ) e. Fin ) |
52 |
51
|
ad2antrl |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( n u. s ) e. Fin ) |
53 |
47 52
|
jca |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( ( n u. s ) C_ c /\ ( n u. s ) e. Fin ) ) |
54 |
|
elin |
|- ( ( n u. s ) e. ( ~P c i^i Fin ) <-> ( ( n u. s ) e. ~P c /\ ( n u. s ) e. Fin ) ) |
55 |
|
vex |
|- c e. _V |
56 |
55
|
elpw2 |
|- ( ( n u. s ) e. ~P c <-> ( n u. s ) C_ c ) |
57 |
56
|
anbi1i |
|- ( ( ( n u. s ) e. ~P c /\ ( n u. s ) e. Fin ) <-> ( ( n u. s ) C_ c /\ ( n u. s ) e. Fin ) ) |
58 |
54 57
|
bitr2i |
|- ( ( ( n u. s ) C_ c /\ ( n u. s ) e. Fin ) <-> ( n u. s ) e. ( ~P c i^i Fin ) ) |
59 |
53 58
|
sylib |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( n u. s ) e. ( ~P c i^i Fin ) ) |
60 |
|
simpllr |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> X = ( S u. T ) ) |
61 |
|
ssun3 |
|- ( S C_ U. n -> S C_ ( U. n u. U. s ) ) |
62 |
|
ssun4 |
|- ( T C_ U. s -> T C_ ( U. n u. U. s ) ) |
63 |
61 62
|
anim12i |
|- ( ( S C_ U. n /\ T C_ U. s ) -> ( S C_ ( U. n u. U. s ) /\ T C_ ( U. n u. U. s ) ) ) |
64 |
63
|
ad2antll |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( S C_ ( U. n u. U. s ) /\ T C_ ( U. n u. U. s ) ) ) |
65 |
|
unss |
|- ( ( S C_ ( U. n u. U. s ) /\ T C_ ( U. n u. U. s ) ) <-> ( S u. T ) C_ ( U. n u. U. s ) ) |
66 |
64 65
|
sylib |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( S u. T ) C_ ( U. n u. U. s ) ) |
67 |
60 66
|
eqsstrd |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> X C_ ( U. n u. U. s ) ) |
68 |
|
uniun |
|- U. ( n u. s ) = ( U. n u. U. s ) |
69 |
67 68
|
sseqtrrdi |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> X C_ U. ( n u. s ) ) |
70 |
|
elpwi |
|- ( c e. ~P J -> c C_ J ) |
71 |
70
|
adantr |
|- ( ( c e. ~P J /\ X = U. c ) -> c C_ J ) |
72 |
71
|
ad2antlr |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> c C_ J ) |
73 |
47 72
|
sstrd |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> ( n u. s ) C_ J ) |
74 |
|
uniss |
|- ( ( n u. s ) C_ J -> U. ( n u. s ) C_ U. J ) |
75 |
74 1
|
sseqtrrdi |
|- ( ( n u. s ) C_ J -> U. ( n u. s ) C_ X ) |
76 |
73 75
|
syl |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> U. ( n u. s ) C_ X ) |
77 |
69 76
|
eqssd |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> X = U. ( n u. s ) ) |
78 |
|
unieq |
|- ( d = ( n u. s ) -> U. d = U. ( n u. s ) ) |
79 |
78
|
rspceeqv |
|- ( ( ( n u. s ) e. ( ~P c i^i Fin ) /\ X = U. ( n u. s ) ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) |
80 |
59 77 79
|
syl2anc |
|- ( ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) /\ ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) /\ ( S C_ U. n /\ T C_ U. s ) ) ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) |
81 |
80
|
exp32 |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( n e. ( ~P c i^i Fin ) /\ s e. ( ~P c i^i Fin ) ) -> ( ( S C_ U. n /\ T C_ U. s ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) |
82 |
81
|
rexlimdvv |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( E. n e. ( ~P c i^i Fin ) E. s e. ( ~P c i^i Fin ) ( S C_ U. n /\ T C_ U. s ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) |
83 |
39 82
|
syl5bir |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( E. n e. ( ~P c i^i Fin ) S C_ U. n /\ E. s e. ( ~P c i^i Fin ) T C_ U. s ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) |
84 |
21 38 83
|
syl2and |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( c e. ~P J /\ X = U. c ) ) -> ( ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) |
85 |
84
|
impancom |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> ( ( c e. ~P J /\ X = U. c ) -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) |
86 |
85
|
expd |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> ( c e. ~P J -> ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) |
87 |
86
|
ralrimiv |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) |
88 |
1
|
iscmp |
|- ( J e. Comp <-> ( J e. Top /\ A. c e. ~P J ( X = U. c -> E. d e. ( ~P c i^i Fin ) X = U. d ) ) ) |
89 |
2 87 88
|
sylanbrc |
|- ( ( ( J e. Top /\ X = ( S u. T ) ) /\ ( ( J |`t S ) e. Comp /\ ( J |`t T ) e. Comp ) ) -> J e. Comp ) |