Step |
Hyp |
Ref |
Expression |
1 |
|
t1connperf.1 |
|- X = U. J |
2 |
|
simplr |
|- ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> J e. Conn ) |
3 |
|
simprr |
|- ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> { x } e. J ) |
4 |
|
vex |
|- x e. _V |
5 |
4
|
snnz |
|- { x } =/= (/) |
6 |
5
|
a1i |
|- ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> { x } =/= (/) ) |
7 |
1
|
t1sncld |
|- ( ( J e. Fre /\ x e. X ) -> { x } e. ( Clsd ` J ) ) |
8 |
7
|
ad2ant2r |
|- ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> { x } e. ( Clsd ` J ) ) |
9 |
1 2 3 6 8
|
connclo |
|- ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> { x } = X ) |
10 |
4
|
ensn1 |
|- { x } ~~ 1o |
11 |
9 10
|
eqbrtrrdi |
|- ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> X ~~ 1o ) |
12 |
11
|
rexlimdvaa |
|- ( ( J e. Fre /\ J e. Conn ) -> ( E. x e. X { x } e. J -> X ~~ 1o ) ) |
13 |
12
|
con3d |
|- ( ( J e. Fre /\ J e. Conn ) -> ( -. X ~~ 1o -> -. E. x e. X { x } e. J ) ) |
14 |
|
ralnex |
|- ( A. x e. X -. { x } e. J <-> -. E. x e. X { x } e. J ) |
15 |
13 14
|
syl6ibr |
|- ( ( J e. Fre /\ J e. Conn ) -> ( -. X ~~ 1o -> A. x e. X -. { x } e. J ) ) |
16 |
|
t1top |
|- ( J e. Fre -> J e. Top ) |
17 |
16
|
adantr |
|- ( ( J e. Fre /\ J e. Conn ) -> J e. Top ) |
18 |
1
|
isperf3 |
|- ( J e. Perf <-> ( J e. Top /\ A. x e. X -. { x } e. J ) ) |
19 |
18
|
baib |
|- ( J e. Top -> ( J e. Perf <-> A. x e. X -. { x } e. J ) ) |
20 |
17 19
|
syl |
|- ( ( J e. Fre /\ J e. Conn ) -> ( J e. Perf <-> A. x e. X -. { x } e. J ) ) |
21 |
15 20
|
sylibrd |
|- ( ( J e. Fre /\ J e. Conn ) -> ( -. X ~~ 1o -> J e. Perf ) ) |
22 |
21
|
3impia |
|- ( ( J e. Fre /\ J e. Conn /\ -. X ~~ 1o ) -> J e. Perf ) |