Metamath Proof Explorer


Theorem rrx2pyel

Description: The y-coordinate of a point in a real Euclidean space of dimension 2 is a real number. (Contributed by AV, 2-Feb-2023)

Ref Expression
Hypotheses rrx2px.i I = 1 2
rrx2px.b P = I
Assertion rrx2pyel X P X 2

Proof

Step Hyp Ref Expression
1 rrx2px.i I = 1 2
2 rrx2px.b P = I
3 id X P X P
4 2ex 2 V
5 4 prid2 2 1 2
6 5 1 eleqtrri 2 I
7 6 a1i X P 2 I
8 2 3 7 mapfvd X P X 2