Step |
Hyp |
Ref |
Expression |
1 |
|
qtopcmp.1 |
β’ π = βͺ π½ |
2 |
|
f1ofo |
β’ ( πΉ : π β1-1-ontoβ π β πΉ : π βontoβ π ) |
3 |
1
|
elqtop2 |
β’ ( ( π½ β TopBases β§ πΉ : π βontoβ π ) β ( π₯ β ( π½ qTop πΉ ) β ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) ) ) |
4 |
1
|
elqtop2 |
β’ ( ( π½ β TopBases β§ πΉ : π βontoβ π ) β ( π¦ β ( π½ qTop πΉ ) β ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) ) |
5 |
3 4
|
anbi12d |
β’ ( ( π½ β TopBases β§ πΉ : π βontoβ π ) β ( ( π₯ β ( π½ qTop πΉ ) β§ π¦ β ( π½ qTop πΉ ) ) β ( ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) ) ) |
6 |
2 5
|
sylan2 |
β’ ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β ( ( π₯ β ( π½ qTop πΉ ) β§ π¦ β ( π½ qTop πΉ ) ) β ( ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) ) ) |
7 |
|
simpl1l |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β π½ β TopBases ) |
8 |
|
simpl2r |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β ( β‘ πΉ β π₯ ) β π½ ) |
9 |
|
simpl3r |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β ( β‘ πΉ β π¦ ) β π½ ) |
10 |
|
simpl1r |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β πΉ : π β1-1-ontoβ π ) |
11 |
|
f1ocnv |
β’ ( πΉ : π β1-1-ontoβ π β β‘ πΉ : π β1-1-ontoβ π ) |
12 |
|
f1ofn |
β’ ( β‘ πΉ : π β1-1-ontoβ π β β‘ πΉ Fn π ) |
13 |
10 11 12
|
3syl |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β β‘ πΉ Fn π ) |
14 |
|
simpl2l |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β π₯ β π ) |
15 |
|
simpr |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β π§ β ( π₯ β© π¦ ) ) |
16 |
15
|
elin1d |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β π§ β π₯ ) |
17 |
|
fnfvima |
β’ ( ( β‘ πΉ Fn π β§ π₯ β π β§ π§ β π₯ ) β ( β‘ πΉ β π§ ) β ( β‘ πΉ β π₯ ) ) |
18 |
13 14 16 17
|
syl3anc |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β ( β‘ πΉ β π§ ) β ( β‘ πΉ β π₯ ) ) |
19 |
|
simpl3l |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β π¦ β π ) |
20 |
15
|
elin2d |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β π§ β π¦ ) |
21 |
|
fnfvima |
β’ ( ( β‘ πΉ Fn π β§ π¦ β π β§ π§ β π¦ ) β ( β‘ πΉ β π§ ) β ( β‘ πΉ β π¦ ) ) |
22 |
13 19 20 21
|
syl3anc |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β ( β‘ πΉ β π§ ) β ( β‘ πΉ β π¦ ) ) |
23 |
18 22
|
elind |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β ( β‘ πΉ β π§ ) β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) |
24 |
|
basis2 |
β’ ( ( ( π½ β TopBases β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( ( β‘ πΉ β π¦ ) β π½ β§ ( β‘ πΉ β π§ ) β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) β β π€ β π½ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) |
25 |
7 8 9 23 24
|
syl22anc |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β β π€ β π½ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) |
26 |
10
|
adantr |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β πΉ : π β1-1-ontoβ π ) |
27 |
|
inss1 |
β’ ( π₯ β© π¦ ) β π₯ |
28 |
|
simp2l |
β’ ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β π₯ β π ) |
29 |
27 28
|
sstrid |
β’ ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β ( π₯ β© π¦ ) β π ) |
30 |
29
|
sselda |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β π§ β π ) |
31 |
30
|
adantr |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β π§ β π ) |
32 |
|
f1ocnvfv2 |
β’ ( ( πΉ : π β1-1-ontoβ π β§ π§ β π ) β ( πΉ β ( β‘ πΉ β π§ ) ) = π§ ) |
33 |
26 31 32
|
syl2anc |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( πΉ β ( β‘ πΉ β π§ ) ) = π§ ) |
34 |
|
f1ofn |
β’ ( πΉ : π β1-1-ontoβ π β πΉ Fn π ) |
35 |
26 34
|
syl |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β πΉ Fn π ) |
36 |
|
simprrr |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) |
37 |
|
inss1 |
β’ ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) β ( β‘ πΉ β π₯ ) |
38 |
36 37
|
sstrdi |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β π€ β ( β‘ πΉ β π₯ ) ) |
39 |
|
cnvimass |
β’ ( β‘ πΉ β π₯ ) β dom πΉ |
40 |
|
f1odm |
β’ ( πΉ : π β1-1-ontoβ π β dom πΉ = π ) |
41 |
26 40
|
syl |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β dom πΉ = π ) |
42 |
39 41
|
sseqtrid |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( β‘ πΉ β π₯ ) β π ) |
43 |
38 42
|
sstrd |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β π€ β π ) |
44 |
|
simprrl |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( β‘ πΉ β π§ ) β π€ ) |
45 |
|
fnfvima |
β’ ( ( πΉ Fn π β§ π€ β π β§ ( β‘ πΉ β π§ ) β π€ ) β ( πΉ β ( β‘ πΉ β π§ ) ) β ( πΉ β π€ ) ) |
46 |
35 43 44 45
|
syl3anc |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( πΉ β ( β‘ πΉ β π§ ) ) β ( πΉ β π€ ) ) |
47 |
33 46
|
eqeltrrd |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β π§ β ( πΉ β π€ ) ) |
48 |
|
imassrn |
β’ ( πΉ β π€ ) β ran πΉ |
49 |
26 2
|
syl |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β πΉ : π βontoβ π ) |
50 |
|
forn |
β’ ( πΉ : π βontoβ π β ran πΉ = π ) |
51 |
49 50
|
syl |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ran πΉ = π ) |
52 |
48 51
|
sseqtrid |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( πΉ β π€ ) β π ) |
53 |
|
f1of1 |
β’ ( πΉ : π β1-1-ontoβ π β πΉ : π β1-1β π ) |
54 |
26 53
|
syl |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β πΉ : π β1-1β π ) |
55 |
|
f1imacnv |
β’ ( ( πΉ : π β1-1β π β§ π€ β π ) β ( β‘ πΉ β ( πΉ β π€ ) ) = π€ ) |
56 |
54 43 55
|
syl2anc |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( β‘ πΉ β ( πΉ β π€ ) ) = π€ ) |
57 |
|
simprl |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β π€ β π½ ) |
58 |
56 57
|
eqeltrd |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( β‘ πΉ β ( πΉ β π€ ) ) β π½ ) |
59 |
7
|
adantr |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β π½ β TopBases ) |
60 |
1
|
elqtop2 |
β’ ( ( π½ β TopBases β§ πΉ : π βontoβ π ) β ( ( πΉ β π€ ) β ( π½ qTop πΉ ) β ( ( πΉ β π€ ) β π β§ ( β‘ πΉ β ( πΉ β π€ ) ) β π½ ) ) ) |
61 |
59 49 60
|
syl2anc |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( ( πΉ β π€ ) β ( π½ qTop πΉ ) β ( ( πΉ β π€ ) β π β§ ( β‘ πΉ β ( πΉ β π€ ) ) β π½ ) ) ) |
62 |
52 58 61
|
mpbir2and |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( πΉ β π€ ) β ( π½ qTop πΉ ) ) |
63 |
|
fnfun |
β’ ( πΉ Fn π β Fun πΉ ) |
64 |
|
inpreima |
β’ ( Fun πΉ β ( β‘ πΉ β ( π₯ β© π¦ ) ) = ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) |
65 |
35 63 64
|
3syl |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( β‘ πΉ β ( π₯ β© π¦ ) ) = ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) |
66 |
36 65
|
sseqtrrd |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β π€ β ( β‘ πΉ β ( π₯ β© π¦ ) ) ) |
67 |
35 63
|
syl |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β Fun πΉ ) |
68 |
38 39
|
sstrdi |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β π€ β dom πΉ ) |
69 |
|
funimass3 |
β’ ( ( Fun πΉ β§ π€ β dom πΉ ) β ( ( πΉ β π€ ) β ( π₯ β© π¦ ) β π€ β ( β‘ πΉ β ( π₯ β© π¦ ) ) ) ) |
70 |
67 68 69
|
syl2anc |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( ( πΉ β π€ ) β ( π₯ β© π¦ ) β π€ β ( β‘ πΉ β ( π₯ β© π¦ ) ) ) ) |
71 |
66 70
|
mpbird |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( πΉ β π€ ) β ( π₯ β© π¦ ) ) |
72 |
|
vex |
β’ π₯ β V |
73 |
72
|
inex1 |
β’ ( π₯ β© π¦ ) β V |
74 |
73
|
elpw2 |
β’ ( ( πΉ β π€ ) β π« ( π₯ β© π¦ ) β ( πΉ β π€ ) β ( π₯ β© π¦ ) ) |
75 |
71 74
|
sylibr |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( πΉ β π€ ) β π« ( π₯ β© π¦ ) ) |
76 |
62 75
|
elind |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β ( πΉ β π€ ) β ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) |
77 |
|
elunii |
β’ ( ( π§ β ( πΉ β π€ ) β§ ( πΉ β π€ ) β ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) β π§ β βͺ ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) |
78 |
47 76 77
|
syl2anc |
β’ ( ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β§ ( π€ β π½ β§ ( ( β‘ πΉ β π§ ) β π€ β§ π€ β ( ( β‘ πΉ β π₯ ) β© ( β‘ πΉ β π¦ ) ) ) ) ) β π§ β βͺ ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) |
79 |
25 78
|
rexlimddv |
β’ ( ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β§ π§ β ( π₯ β© π¦ ) ) β π§ β βͺ ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) |
80 |
79
|
ex |
β’ ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β ( π§ β ( π₯ β© π¦ ) β π§ β βͺ ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) ) |
81 |
80
|
ssrdv |
β’ ( ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β§ ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β ( π₯ β© π¦ ) β βͺ ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) |
82 |
81
|
3expib |
β’ ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β ( ( ( π₯ β π β§ ( β‘ πΉ β π₯ ) β π½ ) β§ ( π¦ β π β§ ( β‘ πΉ β π¦ ) β π½ ) ) β ( π₯ β© π¦ ) β βͺ ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) ) |
83 |
6 82
|
sylbid |
β’ ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β ( ( π₯ β ( π½ qTop πΉ ) β§ π¦ β ( π½ qTop πΉ ) ) β ( π₯ β© π¦ ) β βͺ ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) ) |
84 |
83
|
ralrimivv |
β’ ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β β π₯ β ( π½ qTop πΉ ) β π¦ β ( π½ qTop πΉ ) ( π₯ β© π¦ ) β βͺ ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) |
85 |
|
ovex |
β’ ( π½ qTop πΉ ) β V |
86 |
|
isbasisg |
β’ ( ( π½ qTop πΉ ) β V β ( ( π½ qTop πΉ ) β TopBases β β π₯ β ( π½ qTop πΉ ) β π¦ β ( π½ qTop πΉ ) ( π₯ β© π¦ ) β βͺ ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) ) |
87 |
85 86
|
ax-mp |
β’ ( ( π½ qTop πΉ ) β TopBases β β π₯ β ( π½ qTop πΉ ) β π¦ β ( π½ qTop πΉ ) ( π₯ β© π¦ ) β βͺ ( ( π½ qTop πΉ ) β© π« ( π₯ β© π¦ ) ) ) |
88 |
84 87
|
sylibr |
β’ ( ( π½ β TopBases β§ πΉ : π β1-1-ontoβ π ) β ( π½ qTop πΉ ) β TopBases ) |