| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssel 3976 | . . . . . . . . 9
⊢ (𝐴 ⊆ ℝ → (𝑎 ∈ 𝐴 → 𝑎 ∈ ℝ)) | 
| 2 |  | renegcl 11573 | . . . . . . . . 9
⊢ (𝑎 ∈ ℝ → -𝑎 ∈
ℝ) | 
| 3 | 1, 2 | syl6 35 | . . . . . . . 8
⊢ (𝐴 ⊆ ℝ → (𝑎 ∈ 𝐴 → -𝑎 ∈ ℝ)) | 
| 4 | 3 | ralrimiv 3144 | . . . . . . 7
⊢ (𝐴 ⊆ ℝ →
∀𝑎 ∈ 𝐴 -𝑎 ∈ ℝ) | 
| 5 |  | dmmptg 6261 | . . . . . . 7
⊢
(∀𝑎 ∈
𝐴 -𝑎 ∈ ℝ → dom (𝑎 ∈ 𝐴 ↦ -𝑎) = 𝐴) | 
| 6 | 4, 5 | syl 17 | . . . . . 6
⊢ (𝐴 ⊆ ℝ → dom
(𝑎 ∈ 𝐴 ↦ -𝑎) = 𝐴) | 
| 7 | 6 | eqcomd 2742 | . . . . 5
⊢ (𝐴 ⊆ ℝ → 𝐴 = dom (𝑎 ∈ 𝐴 ↦ -𝑎)) | 
| 8 | 7 | eleq1d 2825 | . . . 4
⊢ (𝐴 ⊆ ℝ → (𝐴 ∈ Fin ↔ dom (𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin)) | 
| 9 |  | funmpt 6603 | . . . . 5
⊢ Fun
(𝑎 ∈ 𝐴 ↦ -𝑎) | 
| 10 |  | fundmfibi 9377 | . . . . 5
⊢ (Fun
(𝑎 ∈ 𝐴 ↦ -𝑎) → ((𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin ↔ dom (𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin)) | 
| 11 | 9, 10 | mp1i 13 | . . . 4
⊢ (𝐴 ⊆ ℝ → ((𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin ↔ dom (𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin)) | 
| 12 | 8, 11 | bitr4d 282 | . . 3
⊢ (𝐴 ⊆ ℝ → (𝐴 ∈ Fin ↔ (𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin)) | 
| 13 |  | reex 11247 | . . . . . 6
⊢ ℝ
∈ V | 
| 14 | 13 | ssex 5320 | . . . . 5
⊢ (𝐴 ⊆ ℝ → 𝐴 ∈ V) | 
| 15 | 14 | mptexd 7245 | . . . 4
⊢ (𝐴 ⊆ ℝ → (𝑎 ∈ 𝐴 ↦ -𝑎) ∈ V) | 
| 16 |  | eqid 2736 | . . . . . 6
⊢ (𝑎 ∈ 𝐴 ↦ -𝑎) = (𝑎 ∈ 𝐴 ↦ -𝑎) | 
| 17 | 16 | negf1o 11694 | . . . . 5
⊢ (𝐴 ⊆ ℝ → (𝑎 ∈ 𝐴 ↦ -𝑎):𝐴–1-1-onto→{𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}) | 
| 18 |  | f1of1 6846 | . . . . 5
⊢ ((𝑎 ∈ 𝐴 ↦ -𝑎):𝐴–1-1-onto→{𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴} → (𝑎 ∈ 𝐴 ↦ -𝑎):𝐴–1-1→{𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}) | 
| 19 | 17, 18 | syl 17 | . . . 4
⊢ (𝐴 ⊆ ℝ → (𝑎 ∈ 𝐴 ↦ -𝑎):𝐴–1-1→{𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}) | 
| 20 |  | f1vrnfibi 9383 | . . . 4
⊢ (((𝑎 ∈ 𝐴 ↦ -𝑎) ∈ V ∧ (𝑎 ∈ 𝐴 ↦ -𝑎):𝐴–1-1→{𝑥 ∈ ℝ ∣ -𝑥 ∈ 𝐴}) → ((𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin ↔ ran (𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin)) | 
| 21 | 15, 19, 20 | syl2anc 584 | . . 3
⊢ (𝐴 ⊆ ℝ → ((𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin ↔ ran (𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin)) | 
| 22 | 1 | imp 406 | . . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℝ) | 
| 23 | 2 | adantl 481 | . . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 ∈ ℝ) → -𝑎 ∈ ℝ) | 
| 24 |  | recn 11246 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℂ) | 
| 25 | 24 | negnegd 11612 | . . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℝ → --𝑎 = 𝑎) | 
| 26 | 25 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℝ → 𝑎 = --𝑎) | 
| 27 | 26 | eleq1d 2825 | . . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℝ → (𝑎 ∈ 𝐴 ↔ --𝑎 ∈ 𝐴)) | 
| 28 | 27 | biimpcd 249 | . . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝐴 → (𝑎 ∈ ℝ → --𝑎 ∈ 𝐴)) | 
| 29 | 28 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ ℝ → --𝑎 ∈ 𝐴)) | 
| 30 | 29 | imp 406 | . . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 ∈ ℝ) → --𝑎 ∈ 𝐴) | 
| 31 | 23, 30 | jca 511 | . . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴) ∧ 𝑎 ∈ ℝ) → (-𝑎 ∈ ℝ ∧ --𝑎 ∈ 𝐴)) | 
| 32 | 22, 31 | mpdan 687 | . . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴) → (-𝑎 ∈ ℝ ∧ --𝑎 ∈ 𝐴)) | 
| 33 |  | eleq1 2828 | . . . . . . . . 9
⊢ (𝑛 = -𝑎 → (𝑛 ∈ ℝ ↔ -𝑎 ∈ ℝ)) | 
| 34 |  | negeq 11501 | . . . . . . . . . 10
⊢ (𝑛 = -𝑎 → -𝑛 = --𝑎) | 
| 35 | 34 | eleq1d 2825 | . . . . . . . . 9
⊢ (𝑛 = -𝑎 → (-𝑛 ∈ 𝐴 ↔ --𝑎 ∈ 𝐴)) | 
| 36 | 33, 35 | anbi12d 632 | . . . . . . . 8
⊢ (𝑛 = -𝑎 → ((𝑛 ∈ ℝ ∧ -𝑛 ∈ 𝐴) ↔ (-𝑎 ∈ ℝ ∧ --𝑎 ∈ 𝐴))) | 
| 37 | 32, 36 | syl5ibrcom 247 | . . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴) → (𝑛 = -𝑎 → (𝑛 ∈ ℝ ∧ -𝑛 ∈ 𝐴))) | 
| 38 |  | simprr 772 | . . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ (𝑛 ∈ ℝ ∧ -𝑛 ∈ 𝐴)) → -𝑛 ∈ 𝐴) | 
| 39 |  | recn 11246 | . . . . . . . . 9
⊢ (𝑛 ∈ ℝ → 𝑛 ∈
ℂ) | 
| 40 |  | negneg 11560 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℂ → --𝑛 = 𝑛) | 
| 41 | 40 | eqcomd 2742 | . . . . . . . . 9
⊢ (𝑛 ∈ ℂ → 𝑛 = --𝑛) | 
| 42 | 39, 41 | syl 17 | . . . . . . . 8
⊢ (𝑛 ∈ ℝ → 𝑛 = --𝑛) | 
| 43 | 42 | ad2antrl 728 | . . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ (𝑛 ∈ ℝ ∧ -𝑛 ∈ 𝐴)) → 𝑛 = --𝑛) | 
| 44 |  | negeq 11501 | . . . . . . . 8
⊢ (𝑎 = -𝑛 → -𝑎 = --𝑛) | 
| 45 | 44 | eqeq2d 2747 | . . . . . . 7
⊢ (𝑎 = -𝑛 → (𝑛 = -𝑎 ↔ 𝑛 = --𝑛)) | 
| 46 | 37, 38, 43, 45 | rspceb2dv 3625 | . . . . . 6
⊢ (𝐴 ⊆ ℝ →
(∃𝑎 ∈ 𝐴 𝑛 = -𝑎 ↔ (𝑛 ∈ ℝ ∧ -𝑛 ∈ 𝐴))) | 
| 47 | 46 | abbidv 2807 | . . . . 5
⊢ (𝐴 ⊆ ℝ → {𝑛 ∣ ∃𝑎 ∈ 𝐴 𝑛 = -𝑎} = {𝑛 ∣ (𝑛 ∈ ℝ ∧ -𝑛 ∈ 𝐴)}) | 
| 48 | 16 | rnmpt 5967 | . . . . 5
⊢ ran
(𝑎 ∈ 𝐴 ↦ -𝑎) = {𝑛 ∣ ∃𝑎 ∈ 𝐴 𝑛 = -𝑎} | 
| 49 |  | df-rab 3436 | . . . . 5
⊢ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} = {𝑛 ∣ (𝑛 ∈ ℝ ∧ -𝑛 ∈ 𝐴)} | 
| 50 | 47, 48, 49 | 3eqtr4g 2801 | . . . 4
⊢ (𝐴 ⊆ ℝ → ran
(𝑎 ∈ 𝐴 ↦ -𝑎) = {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴}) | 
| 51 | 50 | eleq1d 2825 | . . 3
⊢ (𝐴 ⊆ ℝ → (ran
(𝑎 ∈ 𝐴 ↦ -𝑎) ∈ Fin ↔ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ∈ Fin)) | 
| 52 | 12, 21, 51 | 3bitrd 305 | . 2
⊢ (𝐴 ⊆ ℝ → (𝐴 ∈ Fin ↔ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ∈ Fin)) | 
| 53 | 52 | biimpa 476 | 1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin) → {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ∈ Fin) |