Step |
Hyp |
Ref |
Expression |
1 |
|
metcn.2 |
β’ π½ = ( MetOpen β πΆ ) |
2 |
|
metcn.4 |
β’ πΎ = ( MetOpen β π· ) |
3 |
|
txmetcnp.4 |
β’ πΏ = ( MetOpen β πΈ ) |
4 |
|
eqid |
β’ ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) = ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) |
5 |
|
simpl1 |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β πΆ β ( βMet β π ) ) |
6 |
|
simpl2 |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β π· β ( βMet β π ) ) |
7 |
4 5 6
|
tmsxps |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β ( βMet β ( π Γ π ) ) ) |
8 |
|
simpl3 |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β πΈ β ( βMet β π ) ) |
9 |
|
opelxpi |
β’ ( ( π΄ β π β§ π΅ β π ) β β¨ π΄ , π΅ β© β ( π Γ π ) ) |
10 |
9
|
adantl |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β β¨ π΄ , π΅ β© β ( π Γ π ) ) |
11 |
|
eqid |
β’ ( MetOpen β ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) ) = ( MetOpen β ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) ) |
12 |
11 3
|
metcnp |
β’ ( ( ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β ( βMet β ( π Γ π ) ) β§ πΈ β ( βMet β π ) β§ β¨ π΄ , π΅ β© β ( π Γ π ) ) β ( πΉ β ( ( ( MetOpen β ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) ) CnP πΏ ) β β¨ π΄ , π΅ β© ) β ( πΉ : ( π Γ π ) βΆ π β§ β π§ β β+ β π€ β β+ β π₯ β ( π Γ π ) ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) π₯ ) < π€ β ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) < π§ ) ) ) ) |
13 |
7 8 10 12
|
syl3anc |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β ( πΉ β ( ( ( MetOpen β ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) ) CnP πΏ ) β β¨ π΄ , π΅ β© ) β ( πΉ : ( π Γ π ) βΆ π β§ β π§ β β+ β π€ β β+ β π₯ β ( π Γ π ) ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) π₯ ) < π€ β ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) < π§ ) ) ) ) |
14 |
4 5 6 1 2 11
|
tmsxpsmopn |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β ( MetOpen β ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) ) = ( π½ Γt πΎ ) ) |
15 |
14
|
oveq1d |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β ( ( MetOpen β ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) ) CnP πΏ ) = ( ( π½ Γt πΎ ) CnP πΏ ) ) |
16 |
15
|
fveq1d |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β ( ( ( MetOpen β ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) ) CnP πΏ ) β β¨ π΄ , π΅ β© ) = ( ( ( π½ Γt πΎ ) CnP πΏ ) β β¨ π΄ , π΅ β© ) ) |
17 |
16
|
eleq2d |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β ( πΉ β ( ( ( MetOpen β ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) ) CnP πΏ ) β β¨ π΄ , π΅ β© ) β πΉ β ( ( ( π½ Γt πΎ ) CnP πΏ ) β β¨ π΄ , π΅ β© ) ) ) |
18 |
|
oveq2 |
β’ ( π₯ = β¨ π’ , π£ β© β ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) π₯ ) = ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β¨ π’ , π£ β© ) ) |
19 |
18
|
breq1d |
β’ ( π₯ = β¨ π’ , π£ β© β ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) π₯ ) < π€ β ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β¨ π’ , π£ β© ) < π€ ) ) |
20 |
|
df-ov |
β’ ( π΄ πΉ π΅ ) = ( πΉ β β¨ π΄ , π΅ β© ) |
21 |
20
|
oveq1i |
β’ ( ( π΄ πΉ π΅ ) πΈ ( πΉ β π₯ ) ) = ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) |
22 |
|
fveq2 |
β’ ( π₯ = β¨ π’ , π£ β© β ( πΉ β π₯ ) = ( πΉ β β¨ π’ , π£ β© ) ) |
23 |
|
df-ov |
β’ ( π’ πΉ π£ ) = ( πΉ β β¨ π’ , π£ β© ) |
24 |
22 23
|
eqtr4di |
β’ ( π₯ = β¨ π’ , π£ β© β ( πΉ β π₯ ) = ( π’ πΉ π£ ) ) |
25 |
24
|
oveq2d |
β’ ( π₯ = β¨ π’ , π£ β© β ( ( π΄ πΉ π΅ ) πΈ ( πΉ β π₯ ) ) = ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) ) |
26 |
21 25
|
eqtr3id |
β’ ( π₯ = β¨ π’ , π£ β© β ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) = ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) ) |
27 |
26
|
breq1d |
β’ ( π₯ = β¨ π’ , π£ β© β ( ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) < π§ β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) |
28 |
19 27
|
imbi12d |
β’ ( π₯ = β¨ π’ , π£ β© β ( ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) π₯ ) < π€ β ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) < π§ ) β ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β¨ π’ , π£ β© ) < π€ β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) ) |
29 |
28
|
ralxp |
β’ ( β π₯ β ( π Γ π ) ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) π₯ ) < π€ β ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) < π§ ) β β π’ β π β π£ β π ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β¨ π’ , π£ β© ) < π€ β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) |
30 |
5
|
ad2antrr |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β πΆ β ( βMet β π ) ) |
31 |
6
|
ad2antrr |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β π· β ( βMet β π ) ) |
32 |
|
simpllr |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β ( π΄ β π β§ π΅ β π ) ) |
33 |
32
|
simpld |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β π΄ β π ) |
34 |
32
|
simprd |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β π΅ β π ) |
35 |
|
simprrl |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β π’ β π ) |
36 |
|
simprrr |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β π£ β π ) |
37 |
4 30 31 33 34 35 36
|
tmsxpsval2 |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β¨ π’ , π£ β© ) = if ( ( π΄ πΆ π’ ) β€ ( π΅ π· π£ ) , ( π΅ π· π£ ) , ( π΄ πΆ π’ ) ) ) |
38 |
37
|
breq1d |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β¨ π’ , π£ β© ) < π€ β if ( ( π΄ πΆ π’ ) β€ ( π΅ π· π£ ) , ( π΅ π· π£ ) , ( π΄ πΆ π’ ) ) < π€ ) ) |
39 |
|
xmetcl |
β’ ( ( πΆ β ( βMet β π ) β§ π΄ β π β§ π’ β π ) β ( π΄ πΆ π’ ) β β* ) |
40 |
30 33 35 39
|
syl3anc |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β ( π΄ πΆ π’ ) β β* ) |
41 |
|
xmetcl |
β’ ( ( π· β ( βMet β π ) β§ π΅ β π β§ π£ β π ) β ( π΅ π· π£ ) β β* ) |
42 |
31 34 36 41
|
syl3anc |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β ( π΅ π· π£ ) β β* ) |
43 |
|
rpxr |
β’ ( π€ β β+ β π€ β β* ) |
44 |
43
|
ad2antrl |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β π€ β β* ) |
45 |
|
xrmaxlt |
β’ ( ( ( π΄ πΆ π’ ) β β* β§ ( π΅ π· π£ ) β β* β§ π€ β β* ) β ( if ( ( π΄ πΆ π’ ) β€ ( π΅ π· π£ ) , ( π΅ π· π£ ) , ( π΄ πΆ π’ ) ) < π€ β ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) ) ) |
46 |
40 42 44 45
|
syl3anc |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β ( if ( ( π΄ πΆ π’ ) β€ ( π΅ π· π£ ) , ( π΅ π· π£ ) , ( π΄ πΆ π’ ) ) < π€ β ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) ) ) |
47 |
38 46
|
bitrd |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β¨ π’ , π£ β© ) < π€ β ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) ) ) |
48 |
47
|
imbi1d |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ ( π€ β β+ β§ ( π’ β π β§ π£ β π ) ) ) β ( ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β¨ π’ , π£ β© ) < π€ β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) β ( ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) ) |
49 |
48
|
anassrs |
β’ ( ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ π€ β β+ ) β§ ( π’ β π β§ π£ β π ) ) β ( ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β¨ π’ , π£ β© ) < π€ β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) β ( ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) ) |
50 |
49
|
2ralbidva |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ π€ β β+ ) β ( β π’ β π β π£ β π ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) β¨ π’ , π£ β© ) < π€ β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) β β π’ β π β π£ β π ( ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) ) |
51 |
29 50
|
syl5bb |
β’ ( ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β§ π€ β β+ ) β ( β π₯ β ( π Γ π ) ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) π₯ ) < π€ β ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) < π§ ) β β π’ β π β π£ β π ( ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) ) |
52 |
51
|
rexbidva |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β ( β π€ β β+ β π₯ β ( π Γ π ) ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) π₯ ) < π€ β ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) < π§ ) β β π€ β β+ β π’ β π β π£ β π ( ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) ) |
53 |
52
|
ralbidv |
β’ ( ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β§ πΉ : ( π Γ π ) βΆ π ) β ( β π§ β β+ β π€ β β+ β π₯ β ( π Γ π ) ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) π₯ ) < π€ β ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) < π§ ) β β π§ β β+ β π€ β β+ β π’ β π β π£ β π ( ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) ) |
54 |
53
|
pm5.32da |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β ( ( πΉ : ( π Γ π ) βΆ π β§ β π§ β β+ β π€ β β+ β π₯ β ( π Γ π ) ( ( β¨ π΄ , π΅ β© ( dist β ( ( toMetSp β πΆ ) Γs ( toMetSp β π· ) ) ) π₯ ) < π€ β ( ( πΉ β β¨ π΄ , π΅ β© ) πΈ ( πΉ β π₯ ) ) < π§ ) ) β ( πΉ : ( π Γ π ) βΆ π β§ β π§ β β+ β π€ β β+ β π’ β π β π£ β π ( ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) ) ) |
55 |
13 17 54
|
3bitr3d |
β’ ( ( ( πΆ β ( βMet β π ) β§ π· β ( βMet β π ) β§ πΈ β ( βMet β π ) ) β§ ( π΄ β π β§ π΅ β π ) ) β ( πΉ β ( ( ( π½ Γt πΎ ) CnP πΏ ) β β¨ π΄ , π΅ β© ) β ( πΉ : ( π Γ π ) βΆ π β§ β π§ β β+ β π€ β β+ β π’ β π β π£ β π ( ( ( π΄ πΆ π’ ) < π€ β§ ( π΅ π· π£ ) < π€ ) β ( ( π΄ πΉ π΅ ) πΈ ( π’ πΉ π£ ) ) < π§ ) ) ) ) |