Step |
Hyp |
Ref |
Expression |
1 |
|
qtopcmp.1 |
|- X = U. J |
2 |
|
f1ocnv |
|- ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X ) |
3 |
|
f1ofun |
|- ( `' F : Y -1-1-onto-> X -> Fun `' F ) |
4 |
2 3
|
syl |
|- ( F : X -1-1-onto-> Y -> Fun `' F ) |
5 |
4
|
ad2antlr |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> Fun `' F ) |
6 |
|
simpr |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> x C_ Y ) |
7 |
|
df-rn |
|- ran F = dom `' F |
8 |
|
f1ofo |
|- ( F : X -1-1-onto-> Y -> F : X -onto-> Y ) |
9 |
8
|
ad2antlr |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> F : X -onto-> Y ) |
10 |
|
forn |
|- ( F : X -onto-> Y -> ran F = Y ) |
11 |
9 10
|
syl |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ran F = Y ) |
12 |
7 11
|
syl5eqr |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> dom `' F = Y ) |
13 |
6 12
|
sseqtrrd |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> x C_ dom `' F ) |
14 |
|
funimass4 |
|- ( ( Fun `' F /\ x C_ dom `' F ) -> ( ( `' F " x ) C_ U. ( J i^i ~P ( `' F " x ) ) <-> A. y e. x ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) ) ) |
15 |
5 13 14
|
syl2anc |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( ( `' F " x ) C_ U. ( J i^i ~P ( `' F " x ) ) <-> A. y e. x ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) ) ) |
16 |
|
dfss3 |
|- ( x C_ U. ( ( J qTop F ) i^i ~P x ) <-> A. y e. x y e. U. ( ( J qTop F ) i^i ~P x ) ) |
17 |
|
simprl |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> z e. ( ( J qTop F ) i^i ~P x ) ) |
18 |
17
|
elin1d |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> z e. ( J qTop F ) ) |
19 |
1
|
elqtop2 |
|- ( ( J e. TopBases /\ F : X -onto-> Y ) -> ( z e. ( J qTop F ) <-> ( z C_ Y /\ ( `' F " z ) e. J ) ) ) |
20 |
8 19
|
sylan2 |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( z e. ( J qTop F ) <-> ( z C_ Y /\ ( `' F " z ) e. J ) ) ) |
21 |
20
|
ad3antrrr |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( z e. ( J qTop F ) <-> ( z C_ Y /\ ( `' F " z ) e. J ) ) ) |
22 |
18 21
|
mpbid |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( z C_ Y /\ ( `' F " z ) e. J ) ) |
23 |
22
|
simprd |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( `' F " z ) e. J ) |
24 |
17
|
elin2d |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> z e. ~P x ) |
25 |
24
|
elpwid |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> z C_ x ) |
26 |
|
imass2 |
|- ( z C_ x -> ( `' F " z ) C_ ( `' F " x ) ) |
27 |
25 26
|
syl |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( `' F " z ) C_ ( `' F " x ) ) |
28 |
23 27
|
elpwd |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( `' F " z ) e. ~P ( `' F " x ) ) |
29 |
23 28
|
elind |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( `' F " z ) e. ( J i^i ~P ( `' F " x ) ) ) |
30 |
|
simp-4r |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> F : X -1-1-onto-> Y ) |
31 |
30 2
|
syl |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> `' F : Y -1-1-onto-> X ) |
32 |
|
f1ofn |
|- ( `' F : Y -1-1-onto-> X -> `' F Fn Y ) |
33 |
31 32
|
syl |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> `' F Fn Y ) |
34 |
6
|
ad2antrr |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> x C_ Y ) |
35 |
25 34
|
sstrd |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> z C_ Y ) |
36 |
|
simprr |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> y e. z ) |
37 |
|
fnfvima |
|- ( ( `' F Fn Y /\ z C_ Y /\ y e. z ) -> ( `' F ` y ) e. ( `' F " z ) ) |
38 |
33 35 36 37
|
syl3anc |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> ( `' F ` y ) e. ( `' F " z ) ) |
39 |
|
eleq2 |
|- ( w = ( `' F " z ) -> ( ( `' F ` y ) e. w <-> ( `' F ` y ) e. ( `' F " z ) ) ) |
40 |
39
|
rspcev |
|- ( ( ( `' F " z ) e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. ( `' F " z ) ) -> E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w ) |
41 |
29 38 40
|
syl2anc |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( z e. ( ( J qTop F ) i^i ~P x ) /\ y e. z ) ) -> E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w ) |
42 |
41
|
rexlimdvaa |
|- ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) -> ( E. z e. ( ( J qTop F ) i^i ~P x ) y e. z -> E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w ) ) |
43 |
|
simp-4r |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> F : X -1-1-onto-> Y ) |
44 |
|
f1ofun |
|- ( F : X -1-1-onto-> Y -> Fun F ) |
45 |
43 44
|
syl |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> Fun F ) |
46 |
|
simprl |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> w e. ( J i^i ~P ( `' F " x ) ) ) |
47 |
46
|
elin2d |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> w e. ~P ( `' F " x ) ) |
48 |
47
|
elpwid |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> w C_ ( `' F " x ) ) |
49 |
|
funimass2 |
|- ( ( Fun F /\ w C_ ( `' F " x ) ) -> ( F " w ) C_ x ) |
50 |
45 48 49
|
syl2anc |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F " w ) C_ x ) |
51 |
6
|
ad2antrr |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> x C_ Y ) |
52 |
50 51
|
sstrd |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F " w ) C_ Y ) |
53 |
|
f1of1 |
|- ( F : X -1-1-onto-> Y -> F : X -1-1-> Y ) |
54 |
43 53
|
syl |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> F : X -1-1-> Y ) |
55 |
46
|
elin1d |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> w e. J ) |
56 |
|
elssuni |
|- ( w e. J -> w C_ U. J ) |
57 |
56 1
|
sseqtrrdi |
|- ( w e. J -> w C_ X ) |
58 |
55 57
|
syl |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> w C_ X ) |
59 |
|
f1imacnv |
|- ( ( F : X -1-1-> Y /\ w C_ X ) -> ( `' F " ( F " w ) ) = w ) |
60 |
54 58 59
|
syl2anc |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( `' F " ( F " w ) ) = w ) |
61 |
60 55
|
eqeltrd |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( `' F " ( F " w ) ) e. J ) |
62 |
1
|
elqtop2 |
|- ( ( J e. TopBases /\ F : X -onto-> Y ) -> ( ( F " w ) e. ( J qTop F ) <-> ( ( F " w ) C_ Y /\ ( `' F " ( F " w ) ) e. J ) ) ) |
63 |
8 62
|
sylan2 |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( F " w ) e. ( J qTop F ) <-> ( ( F " w ) C_ Y /\ ( `' F " ( F " w ) ) e. J ) ) ) |
64 |
63
|
ad3antrrr |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( ( F " w ) e. ( J qTop F ) <-> ( ( F " w ) C_ Y /\ ( `' F " ( F " w ) ) e. J ) ) ) |
65 |
52 61 64
|
mpbir2and |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F " w ) e. ( J qTop F ) ) |
66 |
|
vex |
|- x e. _V |
67 |
66
|
elpw2 |
|- ( ( F " w ) e. ~P x <-> ( F " w ) C_ x ) |
68 |
50 67
|
sylibr |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F " w ) e. ~P x ) |
69 |
65 68
|
elind |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F " w ) e. ( ( J qTop F ) i^i ~P x ) ) |
70 |
6
|
sselda |
|- ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) -> y e. Y ) |
71 |
70
|
adantr |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> y e. Y ) |
72 |
|
f1ocnvfv2 |
|- ( ( F : X -1-1-onto-> Y /\ y e. Y ) -> ( F ` ( `' F ` y ) ) = y ) |
73 |
43 71 72
|
syl2anc |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F ` ( `' F ` y ) ) = y ) |
74 |
|
f1ofn |
|- ( F : X -1-1-onto-> Y -> F Fn X ) |
75 |
74
|
adantl |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> F Fn X ) |
76 |
75
|
ad3antrrr |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> F Fn X ) |
77 |
|
simprr |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( `' F ` y ) e. w ) |
78 |
|
fnfvima |
|- ( ( F Fn X /\ w C_ X /\ ( `' F ` y ) e. w ) -> ( F ` ( `' F ` y ) ) e. ( F " w ) ) |
79 |
76 58 77 78
|
syl3anc |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> ( F ` ( `' F ` y ) ) e. ( F " w ) ) |
80 |
73 79
|
eqeltrrd |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> y e. ( F " w ) ) |
81 |
|
eleq2 |
|- ( z = ( F " w ) -> ( y e. z <-> y e. ( F " w ) ) ) |
82 |
81
|
rspcev |
|- ( ( ( F " w ) e. ( ( J qTop F ) i^i ~P x ) /\ y e. ( F " w ) ) -> E. z e. ( ( J qTop F ) i^i ~P x ) y e. z ) |
83 |
69 80 82
|
syl2anc |
|- ( ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) /\ ( w e. ( J i^i ~P ( `' F " x ) ) /\ ( `' F ` y ) e. w ) ) -> E. z e. ( ( J qTop F ) i^i ~P x ) y e. z ) |
84 |
83
|
rexlimdvaa |
|- ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) -> ( E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w -> E. z e. ( ( J qTop F ) i^i ~P x ) y e. z ) ) |
85 |
42 84
|
impbid |
|- ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) -> ( E. z e. ( ( J qTop F ) i^i ~P x ) y e. z <-> E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w ) ) |
86 |
|
eluni2 |
|- ( y e. U. ( ( J qTop F ) i^i ~P x ) <-> E. z e. ( ( J qTop F ) i^i ~P x ) y e. z ) |
87 |
|
eluni2 |
|- ( ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) <-> E. w e. ( J i^i ~P ( `' F " x ) ) ( `' F ` y ) e. w ) |
88 |
85 86 87
|
3bitr4g |
|- ( ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) /\ y e. x ) -> ( y e. U. ( ( J qTop F ) i^i ~P x ) <-> ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) ) ) |
89 |
88
|
ralbidva |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( A. y e. x y e. U. ( ( J qTop F ) i^i ~P x ) <-> A. y e. x ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) ) ) |
90 |
16 89
|
syl5bb |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( x C_ U. ( ( J qTop F ) i^i ~P x ) <-> A. y e. x ( `' F ` y ) e. U. ( J i^i ~P ( `' F " x ) ) ) ) |
91 |
15 90
|
bitr4d |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( ( `' F " x ) C_ U. ( J i^i ~P ( `' F " x ) ) <-> x C_ U. ( ( J qTop F ) i^i ~P x ) ) ) |
92 |
|
eltg |
|- ( J e. TopBases -> ( ( `' F " x ) e. ( topGen ` J ) <-> ( `' F " x ) C_ U. ( J i^i ~P ( `' F " x ) ) ) ) |
93 |
92
|
ad2antrr |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( ( `' F " x ) e. ( topGen ` J ) <-> ( `' F " x ) C_ U. ( J i^i ~P ( `' F " x ) ) ) ) |
94 |
|
ovex |
|- ( J qTop F ) e. _V |
95 |
|
eltg |
|- ( ( J qTop F ) e. _V -> ( x e. ( topGen ` ( J qTop F ) ) <-> x C_ U. ( ( J qTop F ) i^i ~P x ) ) ) |
96 |
94 95
|
mp1i |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( x e. ( topGen ` ( J qTop F ) ) <-> x C_ U. ( ( J qTop F ) i^i ~P x ) ) ) |
97 |
91 93 96
|
3bitr4d |
|- ( ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) /\ x C_ Y ) -> ( ( `' F " x ) e. ( topGen ` J ) <-> x e. ( topGen ` ( J qTop F ) ) ) ) |
98 |
97
|
pm5.32da |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( x C_ Y /\ ( `' F " x ) e. ( topGen ` J ) ) <-> ( x C_ Y /\ x e. ( topGen ` ( J qTop F ) ) ) ) ) |
99 |
|
tgtopon |
|- ( J e. TopBases -> ( topGen ` J ) e. ( TopOn ` U. J ) ) |
100 |
99
|
adantr |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( topGen ` J ) e. ( TopOn ` U. J ) ) |
101 |
1
|
fveq2i |
|- ( TopOn ` X ) = ( TopOn ` U. J ) |
102 |
100 101
|
eleqtrrdi |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( topGen ` J ) e. ( TopOn ` X ) ) |
103 |
8
|
adantl |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> F : X -onto-> Y ) |
104 |
|
elqtop3 |
|- ( ( ( topGen ` J ) e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( x e. ( ( topGen ` J ) qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. ( topGen ` J ) ) ) ) |
105 |
102 103 104
|
syl2anc |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( ( topGen ` J ) qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. ( topGen ` J ) ) ) ) |
106 |
|
unitg |
|- ( ( J qTop F ) e. _V -> U. ( topGen ` ( J qTop F ) ) = U. ( J qTop F ) ) |
107 |
94 106
|
ax-mp |
|- U. ( topGen ` ( J qTop F ) ) = U. ( J qTop F ) |
108 |
1
|
elqtop2 |
|- ( ( J e. TopBases /\ F : X -onto-> Y ) -> ( x e. ( J qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. J ) ) ) |
109 |
8 108
|
sylan2 |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( J qTop F ) <-> ( x C_ Y /\ ( `' F " x ) e. J ) ) ) |
110 |
|
simpl |
|- ( ( x C_ Y /\ ( `' F " x ) e. J ) -> x C_ Y ) |
111 |
|
velpw |
|- ( x e. ~P Y <-> x C_ Y ) |
112 |
110 111
|
sylibr |
|- ( ( x C_ Y /\ ( `' F " x ) e. J ) -> x e. ~P Y ) |
113 |
109 112
|
syl6bi |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( J qTop F ) -> x e. ~P Y ) ) |
114 |
113
|
ssrdv |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( J qTop F ) C_ ~P Y ) |
115 |
|
sspwuni |
|- ( ( J qTop F ) C_ ~P Y <-> U. ( J qTop F ) C_ Y ) |
116 |
114 115
|
sylib |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> U. ( J qTop F ) C_ Y ) |
117 |
107 116
|
eqsstrid |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> U. ( topGen ` ( J qTop F ) ) C_ Y ) |
118 |
|
sspwuni |
|- ( ( topGen ` ( J qTop F ) ) C_ ~P Y <-> U. ( topGen ` ( J qTop F ) ) C_ Y ) |
119 |
117 118
|
sylibr |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( topGen ` ( J qTop F ) ) C_ ~P Y ) |
120 |
119
|
sseld |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( topGen ` ( J qTop F ) ) -> x e. ~P Y ) ) |
121 |
120 111
|
syl6ib |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( topGen ` ( J qTop F ) ) -> x C_ Y ) ) |
122 |
121
|
pm4.71rd |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( topGen ` ( J qTop F ) ) <-> ( x C_ Y /\ x e. ( topGen ` ( J qTop F ) ) ) ) ) |
123 |
98 105 122
|
3bitr4d |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( x e. ( ( topGen ` J ) qTop F ) <-> x e. ( topGen ` ( J qTop F ) ) ) ) |
124 |
123
|
eqrdv |
|- ( ( J e. TopBases /\ F : X -1-1-onto-> Y ) -> ( ( topGen ` J ) qTop F ) = ( topGen ` ( J qTop F ) ) ) |