Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
⊢ ( ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) → ( 𝑢 + 𝑥 ) = 𝑥 ) |
2 |
1
|
ralimi |
⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑢 + 𝑥 ) = 𝑥 ) |
3 |
|
simpr |
⊢ ( ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) → ( 𝑥 + 𝑤 ) = 𝑥 ) |
4 |
3
|
ralimi |
⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑤 ) = 𝑥 ) |
5 |
|
oveq1 |
⊢ ( 𝑥 = 𝑢 → ( 𝑥 + 𝑤 ) = ( 𝑢 + 𝑤 ) ) |
6 |
|
id |
⊢ ( 𝑥 = 𝑢 → 𝑥 = 𝑢 ) |
7 |
5 6
|
eqeq12d |
⊢ ( 𝑥 = 𝑢 → ( ( 𝑥 + 𝑤 ) = 𝑥 ↔ ( 𝑢 + 𝑤 ) = 𝑢 ) ) |
8 |
7
|
rspcva |
⊢ ( ( 𝑢 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑤 ) = 𝑥 ) → ( 𝑢 + 𝑤 ) = 𝑢 ) |
9 |
|
oveq2 |
⊢ ( 𝑥 = 𝑤 → ( 𝑢 + 𝑥 ) = ( 𝑢 + 𝑤 ) ) |
10 |
|
id |
⊢ ( 𝑥 = 𝑤 → 𝑥 = 𝑤 ) |
11 |
9 10
|
eqeq12d |
⊢ ( 𝑥 = 𝑤 → ( ( 𝑢 + 𝑥 ) = 𝑥 ↔ ( 𝑢 + 𝑤 ) = 𝑤 ) ) |
12 |
11
|
rspcva |
⊢ ( ( 𝑤 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑢 + 𝑥 ) = 𝑥 ) → ( 𝑢 + 𝑤 ) = 𝑤 ) |
13 |
8 12
|
sylan9req |
⊢ ( ( ( 𝑢 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑤 ) = 𝑥 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑢 + 𝑥 ) = 𝑥 ) ) → 𝑢 = 𝑤 ) |
14 |
13
|
an42s |
⊢ ( ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐵 ( 𝑢 + 𝑥 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑤 ) = 𝑥 ) ) → 𝑢 = 𝑤 ) |
15 |
14
|
ex |
⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( ∀ 𝑥 ∈ 𝐵 ( 𝑢 + 𝑥 ) = 𝑥 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 + 𝑤 ) = 𝑥 ) → 𝑢 = 𝑤 ) ) |
16 |
2 4 15
|
syl2ani |
⊢ ( ( 𝑢 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) ) → 𝑢 = 𝑤 ) ) |
17 |
16
|
rgen2 |
⊢ ∀ 𝑢 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) ) → 𝑢 = 𝑤 ) |
18 |
|
oveq1 |
⊢ ( 𝑢 = 𝑤 → ( 𝑢 + 𝑥 ) = ( 𝑤 + 𝑥 ) ) |
19 |
18
|
eqeq1d |
⊢ ( 𝑢 = 𝑤 → ( ( 𝑢 + 𝑥 ) = 𝑥 ↔ ( 𝑤 + 𝑥 ) = 𝑥 ) ) |
20 |
19
|
ovanraleqv |
⊢ ( 𝑢 = 𝑤 → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) ) ) |
21 |
20
|
rmo4 |
⊢ ( ∃* 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ↔ ∀ 𝑢 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑤 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑤 ) = 𝑥 ) ) → 𝑢 = 𝑤 ) ) |
22 |
17 21
|
mpbir |
⊢ ∃* 𝑢 ∈ 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑢 + 𝑥 ) = 𝑥 ∧ ( 𝑥 + 𝑢 ) = 𝑥 ) |