Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > rrx2pyel | Structured version Visualization version GIF version |
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 |
---|---|
rrx2px.i | ⊢ 𝐼 = {1, 2} |
rrx2px.b | ⊢ 𝑃 = (ℝ ↑m 𝐼) |
Ref | Expression |
---|---|
rrx2pyel | ⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rrx2px.b | . 2 ⊢ 𝑃 = (ℝ ↑m 𝐼) | |
2 | id 22 | . 2 ⊢ (𝑋 ∈ 𝑃 → 𝑋 ∈ 𝑃) | |
3 | 2ex 11786 | . . . . 5 ⊢ 2 ∈ V | |
4 | 3 | prid2 4651 | . . . 4 ⊢ 2 ∈ {1, 2} |
5 | rrx2px.i | . . . 4 ⊢ 𝐼 = {1, 2} | |
6 | 4, 5 | eleqtrri 2832 | . . 3 ⊢ 2 ∈ 𝐼 |
7 | 6 | a1i 11 | . 2 ⊢ (𝑋 ∈ 𝑃 → 2 ∈ 𝐼) |
8 | 1, 2, 7 | mapfvd 8482 | 1 ⊢ (𝑋 ∈ 𝑃 → (𝑋‘2) ∈ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2113 {cpr 4515 ‘cfv 6333 (class class class)co 7164 ↑m cmap 8430 ℝcr 10607 1c1 10609 2c2 11764 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-1cn 10666 ax-addcl 10668 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-iun 4880 df-br 5028 df-opab 5090 df-mpt 5108 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-fv 6341 df-ov 7167 df-oprab 7168 df-mpo 7169 df-1st 7707 df-2nd 7708 df-map 8432 df-2 11772 |
This theorem is referenced by: rrx2pnedifcoorneor 45580 rrx2pnedifcoorneorr 45581 ehl2eudisval0 45589 ehl2eudis0lt 45590 rrx2vlinest 45605 rrx2linest 45606 rrx2linest2 45608 2sphere 45613 2sphere0 45614 line2 45616 line2x 45618 line2y 45619 itsclc0 45635 itsclc0b 45636 itsclinecirc0 45637 itsclinecirc0b 45638 itsclinecirc0in 45639 itscnhlinecirc02plem3 45648 itscnhlinecirc02p 45649 inlinecirc02plem 45650 inlinecirc02p 45651 |
Copyright terms: Public domain | W3C validator |