Step |
Hyp |
Ref |
Expression |
1 |
|
ptbas.1 |
|- B = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } |
2 |
|
ptbasfi.2 |
|- X = X_ n e. A U. ( F ` n ) |
3 |
2
|
ptpjpre1 |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( `' ( w e. X |-> ( w ` I ) ) " U ) = X_ n e. A if ( n = I , U , U. ( F ` n ) ) ) |
4 |
|
simpll |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> A e. V ) |
5 |
|
snfi |
|- { I } e. Fin |
6 |
5
|
a1i |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> { I } e. Fin ) |
7 |
|
simprr |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> U e. ( F ` I ) ) |
8 |
7
|
ad2antrr |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) /\ n = I ) -> U e. ( F ` I ) ) |
9 |
|
simpr |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) /\ n = I ) -> n = I ) |
10 |
9
|
fveq2d |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) /\ n = I ) -> ( F ` n ) = ( F ` I ) ) |
11 |
8 10
|
eleqtrrd |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) /\ n = I ) -> U e. ( F ` n ) ) |
12 |
|
simplr |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> F : A --> Top ) |
13 |
12
|
ffvelrnda |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) -> ( F ` n ) e. Top ) |
14 |
|
eqid |
|- U. ( F ` n ) = U. ( F ` n ) |
15 |
14
|
topopn |
|- ( ( F ` n ) e. Top -> U. ( F ` n ) e. ( F ` n ) ) |
16 |
13 15
|
syl |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) -> U. ( F ` n ) e. ( F ` n ) ) |
17 |
16
|
adantr |
|- ( ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) /\ -. n = I ) -> U. ( F ` n ) e. ( F ` n ) ) |
18 |
11 17
|
ifclda |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. A ) -> if ( n = I , U , U. ( F ` n ) ) e. ( F ` n ) ) |
19 |
|
eldifsni |
|- ( n e. ( A \ { I } ) -> n =/= I ) |
20 |
19
|
neneqd |
|- ( n e. ( A \ { I } ) -> -. n = I ) |
21 |
20
|
adantl |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. ( A \ { I } ) ) -> -. n = I ) |
22 |
21
|
iffalsed |
|- ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ n e. ( A \ { I } ) ) -> if ( n = I , U , U. ( F ` n ) ) = U. ( F ` n ) ) |
23 |
1 4 6 18 22
|
elptr2 |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> X_ n e. A if ( n = I , U , U. ( F ` n ) ) e. B ) |
24 |
3 23
|
eqeltrd |
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( `' ( w e. X |-> ( w ` I ) ) " U ) e. B ) |