Step |
Hyp |
Ref |
Expression |
1 |
|
rrx2pnecoorneor.i |
⊢ 𝐼 = { 1 , 2 } |
2 |
|
rrx2pnecoorneor.b |
⊢ 𝑃 = ( ℝ ↑m 𝐼 ) |
3 |
|
simpr |
⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) |
4 |
1
|
raleqi |
⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ { 1 , 2 } ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ) |
5 |
|
1ex |
⊢ 1 ∈ V |
6 |
|
2ex |
⊢ 2 ∈ V |
7 |
|
fveq2 |
⊢ ( 𝑖 = 1 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 1 ) ) |
8 |
|
fveq2 |
⊢ ( 𝑖 = 1 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 1 ) ) |
9 |
7 8
|
eqeq12d |
⊢ ( 𝑖 = 1 → ( ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) ) |
10 |
|
fveq2 |
⊢ ( 𝑖 = 2 → ( 𝑋 ‘ 𝑖 ) = ( 𝑋 ‘ 2 ) ) |
11 |
|
fveq2 |
⊢ ( 𝑖 = 2 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 2 ) ) |
12 |
10 11
|
eqeq12d |
⊢ ( 𝑖 = 2 → ( ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) |
13 |
5 6 9 12
|
ralpr |
⊢ ( ∀ 𝑖 ∈ { 1 , 2 } ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) |
14 |
4 13
|
bitri |
⊢ ( ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) |
15 |
3 14
|
sylibr |
⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ) |
16 |
|
elmapfn |
⊢ ( 𝑋 ∈ ( ℝ ↑m 𝐼 ) → 𝑋 Fn 𝐼 ) |
17 |
16 2
|
eleq2s |
⊢ ( 𝑋 ∈ 𝑃 → 𝑋 Fn 𝐼 ) |
18 |
|
elmapfn |
⊢ ( 𝑌 ∈ ( ℝ ↑m 𝐼 ) → 𝑌 Fn 𝐼 ) |
19 |
18 2
|
eleq2s |
⊢ ( 𝑌 ∈ 𝑃 → 𝑌 Fn 𝐼 ) |
20 |
17 19
|
anim12i |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼 ) ) |
21 |
20
|
adantr |
⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ( 𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼 ) ) |
22 |
|
eqfnfv |
⊢ ( ( 𝑋 Fn 𝐼 ∧ 𝑌 Fn 𝐼 ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ) ) |
23 |
21 22
|
syl |
⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → ( 𝑋 = 𝑌 ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑋 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) ) ) |
24 |
15 23
|
mpbird |
⊢ ( ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) ∧ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) → 𝑋 = 𝑌 ) |
25 |
24
|
ex |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) → 𝑋 = 𝑌 ) ) |
26 |
25
|
necon3ad |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ≠ 𝑌 → ¬ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) ) |
27 |
26
|
3impia |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ¬ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) |
28 |
|
neorian |
⊢ ( ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ↔ ¬ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) |
29 |
27 28
|
sylibr |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 1 ) ≠ ( 𝑌 ‘ 1 ) ∨ ( 𝑋 ‘ 2 ) ≠ ( 𝑌 ‘ 2 ) ) ) |