| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | f1omptsn.f | . . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ {𝑥}) | 
| 2 |  | eqid 2736 | . . . . . . 7
⊢ {𝑥} = {𝑥} | 
| 3 |  | vsnex 5433 | . . . . . . . 8
⊢ {𝑥} ∈ V | 
| 4 |  | eqsbc1 3834 | . . . . . . . 8
⊢ ({𝑥} ∈ V →
([{𝑥} / 𝑢]𝑢 = {𝑥} ↔ {𝑥} = {𝑥})) | 
| 5 | 3, 4 | ax-mp 5 | . . . . . . 7
⊢
([{𝑥} / 𝑢]𝑢 = {𝑥} ↔ {𝑥} = {𝑥}) | 
| 6 | 2, 5 | mpbir 231 | . . . . . 6
⊢
[{𝑥} / 𝑢]𝑢 = {𝑥} | 
| 7 |  | sbcel2 4417 | . . . . . . . 8
⊢
([{𝑥} / 𝑢]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋{𝑥} / 𝑢⦌𝐴) | 
| 8 |  | csbconstg 3917 | . . . . . . . . . 10
⊢ ({𝑥} ∈ V →
⦋{𝑥} / 𝑢⦌𝐴 = 𝐴) | 
| 9 | 3, 8 | ax-mp 5 | . . . . . . . . 9
⊢
⦋{𝑥} /
𝑢⦌𝐴 = 𝐴 | 
| 10 | 9 | eleq2i 2832 | . . . . . . . 8
⊢ (𝑥 ∈ ⦋{𝑥} / 𝑢⦌𝐴 ↔ 𝑥 ∈ 𝐴) | 
| 11 | 7, 10 | bitri 275 | . . . . . . 7
⊢
([{𝑥} / 𝑢]𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴) | 
| 12 |  | f1omptsn.r | . . . . . . . . . . . . . 14
⊢ 𝑅 = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} | 
| 13 | 12 | eqabri 2884 | . . . . . . . . . . . . 13
⊢ (𝑢 ∈ 𝑅 ↔ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}) | 
| 14 |  | df-rex 3070 | . . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐴 𝑢 = {𝑥} ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥})) | 
| 15 | 13, 14 | sylbbr 236 | . . . . . . . . . . . 12
⊢
(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥}) → 𝑢 ∈ 𝑅) | 
| 16 | 15 | 19.23bi 2190 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥}) → 𝑢 ∈ 𝑅) | 
| 17 | 16 | sbcth 3802 | . . . . . . . . . 10
⊢ ({𝑥} ∈ V → [{𝑥} / 𝑢]((𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥}) → 𝑢 ∈ 𝑅)) | 
| 18 | 3, 17 | ax-mp 5 | . . . . . . . . 9
⊢
[{𝑥} / 𝑢]((𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥}) → 𝑢 ∈ 𝑅) | 
| 19 |  | sbcimg 3836 | . . . . . . . . . 10
⊢ ({𝑥} ∈ V →
([{𝑥} / 𝑢]((𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥}) → 𝑢 ∈ 𝑅) ↔ ([{𝑥} / 𝑢](𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥}) → [{𝑥} / 𝑢]𝑢 ∈ 𝑅))) | 
| 20 | 3, 19 | ax-mp 5 | . . . . . . . . 9
⊢
([{𝑥} / 𝑢]((𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥}) → 𝑢 ∈ 𝑅) ↔ ([{𝑥} / 𝑢](𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥}) → [{𝑥} / 𝑢]𝑢 ∈ 𝑅)) | 
| 21 | 18, 20 | mpbi 230 | . . . . . . . 8
⊢
([{𝑥} / 𝑢](𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥}) → [{𝑥} / 𝑢]𝑢 ∈ 𝑅) | 
| 22 |  | sbcan 3837 | . . . . . . . 8
⊢
([{𝑥} / 𝑢](𝑥 ∈ 𝐴 ∧ 𝑢 = {𝑥}) ↔ ([{𝑥} / 𝑢]𝑥 ∈ 𝐴 ∧ [{𝑥} / 𝑢]𝑢 = {𝑥})) | 
| 23 |  | sbcel1v 3855 | . . . . . . . 8
⊢
([{𝑥} / 𝑢]𝑢 ∈ 𝑅 ↔ {𝑥} ∈ 𝑅) | 
| 24 | 21, 22, 23 | 3imtr3i 291 | . . . . . . 7
⊢
(([{𝑥} /
𝑢]𝑥 ∈ 𝐴 ∧ [{𝑥} / 𝑢]𝑢 = {𝑥}) → {𝑥} ∈ 𝑅) | 
| 25 | 11, 24 | sylanbr 582 | . . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ [{𝑥} / 𝑢]𝑢 = {𝑥}) → {𝑥} ∈ 𝑅) | 
| 26 | 6, 25 | mpan2 691 | . . . . 5
⊢ (𝑥 ∈ 𝐴 → {𝑥} ∈ 𝑅) | 
| 27 | 1, 26 | fmpti 7131 | . . . 4
⊢ 𝐹:𝐴⟶𝑅 | 
| 28 | 1 | fvmpt2 7026 | . . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ {𝑥} ∈ 𝑅) → (𝐹‘𝑥) = {𝑥}) | 
| 29 | 26, 28 | mpdan 687 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = {𝑥}) | 
| 30 |  | sneq 4635 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) | 
| 31 | 30, 1, 3 | fvmpt3i 7020 | . . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = {𝑦}) | 
| 32 | 29, 31 | eqeqan12d 2750 | . . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ {𝑥} = {𝑦})) | 
| 33 |  | vex 3483 | . . . . . . . 8
⊢ 𝑥 ∈ V | 
| 34 |  | sneqbg 4842 | . . . . . . . 8
⊢ (𝑥 ∈ V → ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦)) | 
| 35 | 33, 34 | ax-mp 5 | . . . . . . 7
⊢ ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦) | 
| 36 | 32, 35 | bitrdi 287 | . . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ 𝑥 = 𝑦)) | 
| 37 | 36 | biimpd 229 | . . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) | 
| 38 | 37 | rgen2 3198 | . . . 4
⊢
∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) | 
| 39 |  | dff13 7276 | . . . 4
⊢ (𝐹:𝐴–1-1→𝑅 ↔ (𝐹:𝐴⟶𝑅 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) | 
| 40 | 27, 38, 39 | mpbir2an 711 | . . 3
⊢ 𝐹:𝐴–1-1→𝑅 | 
| 41 |  | f1f1orn 6858 | . . 3
⊢ (𝐹:𝐴–1-1→𝑅 → 𝐹:𝐴–1-1-onto→ran
𝐹) | 
| 42 | 40, 41 | ax-mp 5 | . 2
⊢ 𝐹:𝐴–1-1-onto→ran
𝐹 | 
| 43 |  | rnmptsn 37337 | . . . 4
⊢ ran
(𝑥 ∈ 𝐴 ↦ {𝑥}) = {𝑢 ∣ ∃𝑥 ∈ 𝐴 𝑢 = {𝑥}} | 
| 44 | 1 | rneqi 5947 | . . . 4
⊢ ran 𝐹 = ran (𝑥 ∈ 𝐴 ↦ {𝑥}) | 
| 45 | 43, 44, 12 | 3eqtr4i 2774 | . . 3
⊢ ran 𝐹 = 𝑅 | 
| 46 |  | f1oeq3 6837 | . . 3
⊢ (ran
𝐹 = 𝑅 → (𝐹:𝐴–1-1-onto→ran
𝐹 ↔ 𝐹:𝐴–1-1-onto→𝑅)) | 
| 47 | 45, 46 | ax-mp 5 | . 2
⊢ (𝐹:𝐴–1-1-onto→ran
𝐹 ↔ 𝐹:𝐴–1-1-onto→𝑅) | 
| 48 | 42, 47 | mpbi 230 | 1
⊢ 𝐹:𝐴–1-1-onto→𝑅 |