Step |
Hyp |
Ref |
Expression |
1 |
|
heibor.1 |
β’ π½ = ( MetOpen β π· ) |
2 |
|
heibor.3 |
β’ πΎ = { π’ β£ Β¬ β π£ β ( π« π β© Fin ) π’ β βͺ π£ } |
3 |
|
heibor.4 |
β’ πΊ = { β¨ π¦ , π β© β£ ( π β β0 β§ π¦ β ( πΉ β π ) β§ ( π¦ π΅ π ) β πΎ ) } |
4 |
|
heibor.5 |
β’ π΅ = ( π§ β π , π β β0 β¦ ( π§ ( ball β π· ) ( 1 / ( 2 β π ) ) ) ) |
5 |
|
heibor.6 |
β’ ( π β π· β ( CMet β π ) ) |
6 |
|
heibor.7 |
β’ ( π β πΉ : β0 βΆ ( π« π β© Fin ) ) |
7 |
|
heibor.8 |
β’ ( π β β π β β0 π = βͺ π¦ β ( πΉ β π ) ( π¦ π΅ π ) ) |
8 |
|
0nn0 |
β’ 0 β β0 |
9 |
|
inss2 |
β’ ( π« π β© Fin ) β Fin |
10 |
|
ffvelcdm |
β’ ( ( πΉ : β0 βΆ ( π« π β© Fin ) β§ 0 β β0 ) β ( πΉ β 0 ) β ( π« π β© Fin ) ) |
11 |
9 10
|
sselid |
β’ ( ( πΉ : β0 βΆ ( π« π β© Fin ) β§ 0 β β0 ) β ( πΉ β 0 ) β Fin ) |
12 |
6 8 11
|
sylancl |
β’ ( π β ( πΉ β 0 ) β Fin ) |
13 |
|
fveq2 |
β’ ( π = 0 β ( πΉ β π ) = ( πΉ β 0 ) ) |
14 |
|
oveq2 |
β’ ( π = 0 β ( π¦ π΅ π ) = ( π¦ π΅ 0 ) ) |
15 |
13 14
|
iuneq12d |
β’ ( π = 0 β βͺ π¦ β ( πΉ β π ) ( π¦ π΅ π ) = βͺ π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) ) |
16 |
15
|
eqeq2d |
β’ ( π = 0 β ( π = βͺ π¦ β ( πΉ β π ) ( π¦ π΅ π ) β π = βͺ π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) ) ) |
17 |
16
|
rspccva |
β’ ( ( β π β β0 π = βͺ π¦ β ( πΉ β π ) ( π¦ π΅ π ) β§ 0 β β0 ) β π = βͺ π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) ) |
18 |
7 8 17
|
sylancl |
β’ ( π β π = βͺ π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) ) |
19 |
|
eqimss |
β’ ( π = βͺ π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) β π β βͺ π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) ) |
20 |
18 19
|
syl |
β’ ( π β π β βͺ π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) ) |
21 |
|
ovex |
β’ ( π¦ π΅ 0 ) β V |
22 |
1 2 21
|
heiborlem1 |
β’ ( ( ( πΉ β 0 ) β Fin β§ π β βͺ π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) β§ π β πΎ ) β β π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) β πΎ ) |
23 |
|
oveq1 |
β’ ( π¦ = π₯ β ( π¦ π΅ 0 ) = ( π₯ π΅ 0 ) ) |
24 |
23
|
eleq1d |
β’ ( π¦ = π₯ β ( ( π¦ π΅ 0 ) β πΎ β ( π₯ π΅ 0 ) β πΎ ) ) |
25 |
24
|
cbvrexvw |
β’ ( β π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) β πΎ β β π₯ β ( πΉ β 0 ) ( π₯ π΅ 0 ) β πΎ ) |
26 |
22 25
|
sylib |
β’ ( ( ( πΉ β 0 ) β Fin β§ π β βͺ π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) β§ π β πΎ ) β β π₯ β ( πΉ β 0 ) ( π₯ π΅ 0 ) β πΎ ) |
27 |
26
|
3expia |
β’ ( ( ( πΉ β 0 ) β Fin β§ π β βͺ π¦ β ( πΉ β 0 ) ( π¦ π΅ 0 ) ) β ( π β πΎ β β π₯ β ( πΉ β 0 ) ( π₯ π΅ 0 ) β πΎ ) ) |
28 |
12 20 27
|
syl2anc |
β’ ( π β ( π β πΎ β β π₯ β ( πΉ β 0 ) ( π₯ π΅ 0 ) β πΎ ) ) |
29 |
28
|
adantr |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β ( π β πΎ β β π₯ β ( πΉ β 0 ) ( π₯ π΅ 0 ) β πΎ ) ) |
30 |
|
vex |
β’ π₯ β V |
31 |
|
c0ex |
β’ 0 β V |
32 |
1 2 3 30 31
|
heiborlem2 |
β’ ( π₯ πΊ 0 β ( 0 β β0 β§ π₯ β ( πΉ β 0 ) β§ ( π₯ π΅ 0 ) β πΎ ) ) |
33 |
1 2 3 4 5 6 7
|
heiborlem3 |
β’ ( π β β π β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) |
34 |
33
|
ad2antrr |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ π₯ πΊ 0 ) β β π β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) |
35 |
5
|
ad2antrr |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ ( π₯ πΊ 0 β§ β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) ) β π· β ( CMet β π ) ) |
36 |
6
|
ad2antrr |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ ( π₯ πΊ 0 β§ β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) ) β πΉ : β0 βΆ ( π« π β© Fin ) ) |
37 |
7
|
ad2antrr |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ ( π₯ πΊ 0 β§ β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) ) β β π β β0 π = βͺ π¦ β ( πΉ β π ) ( π¦ π΅ π ) ) |
38 |
|
simprr |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ ( π₯ πΊ 0 β§ β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) ) β β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) |
39 |
|
fveq2 |
β’ ( π₯ = π‘ β ( π β π₯ ) = ( π β π‘ ) ) |
40 |
|
fveq2 |
β’ ( π₯ = π‘ β ( 2nd β π₯ ) = ( 2nd β π‘ ) ) |
41 |
40
|
oveq1d |
β’ ( π₯ = π‘ β ( ( 2nd β π₯ ) + 1 ) = ( ( 2nd β π‘ ) + 1 ) ) |
42 |
39 41
|
breq12d |
β’ ( π₯ = π‘ β ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β ( π β π‘ ) πΊ ( ( 2nd β π‘ ) + 1 ) ) ) |
43 |
|
fveq2 |
β’ ( π₯ = π‘ β ( π΅ β π₯ ) = ( π΅ β π‘ ) ) |
44 |
39 41
|
oveq12d |
β’ ( π₯ = π‘ β ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) = ( ( π β π‘ ) π΅ ( ( 2nd β π‘ ) + 1 ) ) ) |
45 |
43 44
|
ineq12d |
β’ ( π₯ = π‘ β ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) = ( ( π΅ β π‘ ) β© ( ( π β π‘ ) π΅ ( ( 2nd β π‘ ) + 1 ) ) ) ) |
46 |
45
|
eleq1d |
β’ ( π₯ = π‘ β ( ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ β ( ( π΅ β π‘ ) β© ( ( π β π‘ ) π΅ ( ( 2nd β π‘ ) + 1 ) ) ) β πΎ ) ) |
47 |
42 46
|
anbi12d |
β’ ( π₯ = π‘ β ( ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) β ( ( π β π‘ ) πΊ ( ( 2nd β π‘ ) + 1 ) β§ ( ( π΅ β π‘ ) β© ( ( π β π‘ ) π΅ ( ( 2nd β π‘ ) + 1 ) ) ) β πΎ ) ) ) |
48 |
47
|
cbvralvw |
β’ ( β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) β β π‘ β πΊ ( ( π β π‘ ) πΊ ( ( 2nd β π‘ ) + 1 ) β§ ( ( π΅ β π‘ ) β© ( ( π β π‘ ) π΅ ( ( 2nd β π‘ ) + 1 ) ) ) β πΎ ) ) |
49 |
38 48
|
sylib |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ ( π₯ πΊ 0 β§ β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) ) β β π‘ β πΊ ( ( π β π‘ ) πΊ ( ( 2nd β π‘ ) + 1 ) β§ ( ( π΅ β π‘ ) β© ( ( π β π‘ ) π΅ ( ( 2nd β π‘ ) + 1 ) ) ) β πΎ ) ) |
50 |
|
simprl |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ ( π₯ πΊ 0 β§ β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) ) β π₯ πΊ 0 ) |
51 |
|
eqeq1 |
β’ ( π = π β ( π = 0 β π = 0 ) ) |
52 |
|
oveq1 |
β’ ( π = π β ( π β 1 ) = ( π β 1 ) ) |
53 |
51 52
|
ifbieq2d |
β’ ( π = π β if ( π = 0 , π₯ , ( π β 1 ) ) = if ( π = 0 , π₯ , ( π β 1 ) ) ) |
54 |
53
|
cbvmptv |
β’ ( π β β0 β¦ if ( π = 0 , π₯ , ( π β 1 ) ) ) = ( π β β0 β¦ if ( π = 0 , π₯ , ( π β 1 ) ) ) |
55 |
|
seqeq3 |
β’ ( ( π β β0 β¦ if ( π = 0 , π₯ , ( π β 1 ) ) ) = ( π β β0 β¦ if ( π = 0 , π₯ , ( π β 1 ) ) ) β seq 0 ( π , ( π β β0 β¦ if ( π = 0 , π₯ , ( π β 1 ) ) ) ) = seq 0 ( π , ( π β β0 β¦ if ( π = 0 , π₯ , ( π β 1 ) ) ) ) ) |
56 |
54 55
|
ax-mp |
β’ seq 0 ( π , ( π β β0 β¦ if ( π = 0 , π₯ , ( π β 1 ) ) ) ) = seq 0 ( π , ( π β β0 β¦ if ( π = 0 , π₯ , ( π β 1 ) ) ) ) |
57 |
|
eqid |
β’ ( π β β β¦ β¨ ( seq 0 ( π , ( π β β0 β¦ if ( π = 0 , π₯ , ( π β 1 ) ) ) ) β π ) , ( 3 / ( 2 β π ) ) β© ) = ( π β β β¦ β¨ ( seq 0 ( π , ( π β β0 β¦ if ( π = 0 , π₯ , ( π β 1 ) ) ) ) β π ) , ( 3 / ( 2 β π ) ) β© ) |
58 |
|
simplrl |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ ( π₯ πΊ 0 β§ β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) ) β π β π½ ) |
59 |
|
cmetmet |
β’ ( π· β ( CMet β π ) β π· β ( Met β π ) ) |
60 |
|
metxmet |
β’ ( π· β ( Met β π ) β π· β ( βMet β π ) ) |
61 |
1
|
mopnuni |
β’ ( π· β ( βMet β π ) β π = βͺ π½ ) |
62 |
5 59 60 61
|
4syl |
β’ ( π β π = βͺ π½ ) |
63 |
62
|
adantr |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β π = βͺ π½ ) |
64 |
|
simprr |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β βͺ π½ = βͺ π ) |
65 |
63 64
|
eqtr2d |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β βͺ π = π ) |
66 |
65
|
adantr |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ ( π₯ πΊ 0 β§ β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) ) β βͺ π = π ) |
67 |
1 2 3 4 35 36 37 49 50 56 57 58 66
|
heiborlem9 |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ ( π₯ πΊ 0 β§ β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) ) ) β Β¬ π β πΎ ) |
68 |
67
|
expr |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ π₯ πΊ 0 ) β ( β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) β Β¬ π β πΎ ) ) |
69 |
68
|
exlimdv |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ π₯ πΊ 0 ) β ( β π β π₯ β πΊ ( ( π β π₯ ) πΊ ( ( 2nd β π₯ ) + 1 ) β§ ( ( π΅ β π₯ ) β© ( ( π β π₯ ) π΅ ( ( 2nd β π₯ ) + 1 ) ) ) β πΎ ) β Β¬ π β πΎ ) ) |
70 |
34 69
|
mpd |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ π₯ πΊ 0 ) β Β¬ π β πΎ ) |
71 |
32 70
|
sylan2br |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ ( 0 β β0 β§ π₯ β ( πΉ β 0 ) β§ ( π₯ π΅ 0 ) β πΎ ) ) β Β¬ π β πΎ ) |
72 |
71
|
3exp2 |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β ( 0 β β0 β ( π₯ β ( πΉ β 0 ) β ( ( π₯ π΅ 0 ) β πΎ β Β¬ π β πΎ ) ) ) ) |
73 |
8 72
|
mpi |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β ( π₯ β ( πΉ β 0 ) β ( ( π₯ π΅ 0 ) β πΎ β Β¬ π β πΎ ) ) ) |
74 |
73
|
rexlimdv |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β ( β π₯ β ( πΉ β 0 ) ( π₯ π΅ 0 ) β πΎ β Β¬ π β πΎ ) ) |
75 |
29 74
|
syld |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β ( π β πΎ β Β¬ π β πΎ ) ) |
76 |
75
|
pm2.01d |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β Β¬ π β πΎ ) |
77 |
|
elfvdm |
β’ ( π· β ( CMet β π ) β π β dom CMet ) |
78 |
|
sseq1 |
β’ ( π’ = π β ( π’ β βͺ π£ β π β βͺ π£ ) ) |
79 |
78
|
rexbidv |
β’ ( π’ = π β ( β π£ β ( π« π β© Fin ) π’ β βͺ π£ β β π£ β ( π« π β© Fin ) π β βͺ π£ ) ) |
80 |
79
|
notbid |
β’ ( π’ = π β ( Β¬ β π£ β ( π« π β© Fin ) π’ β βͺ π£ β Β¬ β π£ β ( π« π β© Fin ) π β βͺ π£ ) ) |
81 |
80 2
|
elab2g |
β’ ( π β dom CMet β ( π β πΎ β Β¬ β π£ β ( π« π β© Fin ) π β βͺ π£ ) ) |
82 |
5 77 81
|
3syl |
β’ ( π β ( π β πΎ β Β¬ β π£ β ( π« π β© Fin ) π β βͺ π£ ) ) |
83 |
82
|
adantr |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β ( π β πΎ β Β¬ β π£ β ( π« π β© Fin ) π β βͺ π£ ) ) |
84 |
83
|
con2bid |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β ( β π£ β ( π« π β© Fin ) π β βͺ π£ β Β¬ π β πΎ ) ) |
85 |
76 84
|
mpbird |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β β π£ β ( π« π β© Fin ) π β βͺ π£ ) |
86 |
62
|
ad2antrr |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ π£ β ( π« π β© Fin ) ) β π = βͺ π½ ) |
87 |
86
|
sseq1d |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ π£ β ( π« π β© Fin ) ) β ( π β βͺ π£ β βͺ π½ β βͺ π£ ) ) |
88 |
|
inss1 |
β’ ( π« π β© Fin ) β π« π |
89 |
88
|
sseli |
β’ ( π£ β ( π« π β© Fin ) β π£ β π« π ) |
90 |
89
|
elpwid |
β’ ( π£ β ( π« π β© Fin ) β π£ β π ) |
91 |
|
simprl |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β π β π½ ) |
92 |
|
sstr |
β’ ( ( π£ β π β§ π β π½ ) β π£ β π½ ) |
93 |
92
|
unissd |
β’ ( ( π£ β π β§ π β π½ ) β βͺ π£ β βͺ π½ ) |
94 |
90 91 93
|
syl2anr |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ π£ β ( π« π β© Fin ) ) β βͺ π£ β βͺ π½ ) |
95 |
94
|
biantrud |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ π£ β ( π« π β© Fin ) ) β ( βͺ π½ β βͺ π£ β ( βͺ π½ β βͺ π£ β§ βͺ π£ β βͺ π½ ) ) ) |
96 |
|
eqss |
β’ ( βͺ π½ = βͺ π£ β ( βͺ π½ β βͺ π£ β§ βͺ π£ β βͺ π½ ) ) |
97 |
95 96
|
bitr4di |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ π£ β ( π« π β© Fin ) ) β ( βͺ π½ β βͺ π£ β βͺ π½ = βͺ π£ ) ) |
98 |
87 97
|
bitrd |
β’ ( ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β§ π£ β ( π« π β© Fin ) ) β ( π β βͺ π£ β βͺ π½ = βͺ π£ ) ) |
99 |
98
|
rexbidva |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β ( β π£ β ( π« π β© Fin ) π β βͺ π£ β β π£ β ( π« π β© Fin ) βͺ π½ = βͺ π£ ) ) |
100 |
85 99
|
mpbid |
β’ ( ( π β§ ( π β π½ β§ βͺ π½ = βͺ π ) ) β β π£ β ( π« π β© Fin ) βͺ π½ = βͺ π£ ) |