Step |
Hyp |
Ref |
Expression |
1 |
|
metxmet |
β’ ( π· β ( Met β π ) β π· β ( βMet β π ) ) |
2 |
|
xmetres2 |
β’ ( ( π· β ( βMet β π ) β§ π
β π ) β ( π· βΎ ( π
Γ π
) ) β ( βMet β π
) ) |
3 |
1 2
|
sylan |
β’ ( ( π· β ( Met β π ) β§ π
β π ) β ( π· βΎ ( π
Γ π
) ) β ( βMet β π
) ) |
4 |
|
metf |
β’ ( π· β ( Met β π ) β π· : ( π Γ π ) βΆ β ) |
5 |
4
|
adantr |
β’ ( ( π· β ( Met β π ) β§ π
β π ) β π· : ( π Γ π ) βΆ β ) |
6 |
|
simpr |
β’ ( ( π· β ( Met β π ) β§ π
β π ) β π
β π ) |
7 |
|
xpss12 |
β’ ( ( π
β π β§ π
β π ) β ( π
Γ π
) β ( π Γ π ) ) |
8 |
6 7
|
sylancom |
β’ ( ( π· β ( Met β π ) β§ π
β π ) β ( π
Γ π
) β ( π Γ π ) ) |
9 |
5 8
|
fssresd |
β’ ( ( π· β ( Met β π ) β§ π
β π ) β ( π· βΎ ( π
Γ π
) ) : ( π
Γ π
) βΆ β ) |
10 |
|
ismet2 |
β’ ( ( π· βΎ ( π
Γ π
) ) β ( Met β π
) β ( ( π· βΎ ( π
Γ π
) ) β ( βMet β π
) β§ ( π· βΎ ( π
Γ π
) ) : ( π
Γ π
) βΆ β ) ) |
11 |
3 9 10
|
sylanbrc |
β’ ( ( π· β ( Met β π ) β§ π
β π ) β ( π· βΎ ( π
Γ π
) ) β ( Met β π
) ) |