| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fsetfocdm.f | . . . 4
⊢ 𝐹 = {𝑓 ∣ 𝑓:𝐴⟶𝐵} | 
| 2 |  | fsetfocdm.s | . . . 4
⊢ 𝑆 = (𝑔 ∈ 𝐹 ↦ (𝑔‘𝑋)) | 
| 3 | 1, 2 | fsetfcdm 8900 | . . 3
⊢ (𝑋 ∈ 𝐴 → 𝑆:𝐹⟶𝐵) | 
| 4 | 3 | adantl 481 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → 𝑆:𝐹⟶𝐵) | 
| 5 |  | simplr 769 | . . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ 𝐵) | 
| 6 | 5 | fmpttd 7135 | . . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝑔):𝐴⟶𝐵) | 
| 7 |  | simpll 767 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → 𝐴 ∈ 𝑉) | 
| 8 | 7 | mptexd 7244 | . . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝑔) ∈ V) | 
| 9 |  | feq1 6716 | . . . . . . 7
⊢ (𝑓 = (𝑥 ∈ 𝐴 ↦ 𝑔) → (𝑓:𝐴⟶𝐵 ↔ (𝑥 ∈ 𝐴 ↦ 𝑔):𝐴⟶𝐵)) | 
| 10 | 9, 1 | elab2g 3680 | . . . . . 6
⊢ ((𝑥 ∈ 𝐴 ↦ 𝑔) ∈ V → ((𝑥 ∈ 𝐴 ↦ 𝑔) ∈ 𝐹 ↔ (𝑥 ∈ 𝐴 ↦ 𝑔):𝐴⟶𝐵)) | 
| 11 | 8, 10 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑔) ∈ 𝐹 ↔ (𝑥 ∈ 𝐴 ↦ 𝑔):𝐴⟶𝐵)) | 
| 12 | 6, 11 | mpbird 257 | . . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝑔) ∈ 𝐹) | 
| 13 |  | fveq1 6905 | . . . . . . . . 9
⊢ (𝑔 = 𝑓 → (𝑔‘𝑋) = (𝑓‘𝑋)) | 
| 14 | 13 | cbvmptv 5255 | . . . . . . . 8
⊢ (𝑔 ∈ 𝐹 ↦ (𝑔‘𝑋)) = (𝑓 ∈ 𝐹 ↦ (𝑓‘𝑋)) | 
| 15 | 2, 14 | eqtri 2765 | . . . . . . 7
⊢ 𝑆 = (𝑓 ∈ 𝐹 ↦ (𝑓‘𝑋)) | 
| 16 |  | fveq1 6905 | . . . . . . 7
⊢ (𝑓 = (𝑥 ∈ 𝐴 ↦ 𝑔) → (𝑓‘𝑋) = ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋)) | 
| 17 |  | fvexd 6921 | . . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋) ∈ V) | 
| 18 | 15, 16, 12, 17 | fvmptd3 7039 | . . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → (𝑆‘(𝑥 ∈ 𝐴 ↦ 𝑔)) = ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋)) | 
| 19 |  | eqidd 2738 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → 𝑔 = 𝑔) | 
| 20 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ 𝑔) = (𝑥 ∈ 𝐴 ↦ 𝑔) | 
| 21 |  | vex 3484 | . . . . . . . 8
⊢ 𝑔 ∈ V | 
| 22 | 19, 20, 21 | fvmpt 7016 | . . . . . . 7
⊢ (𝑋 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋) = 𝑔) | 
| 23 | 22 | ad2antlr 727 | . . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋) = 𝑔) | 
| 24 | 18, 23 | eqtrd 2777 | . . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → (𝑆‘(𝑥 ∈ 𝐴 ↦ 𝑔)) = 𝑔) | 
| 25 |  | fveq2 6906 | . . . . . 6
⊢ (ℎ = (𝑥 ∈ 𝐴 ↦ 𝑔) → (𝑆‘ℎ) = (𝑆‘(𝑥 ∈ 𝐴 ↦ 𝑔))) | 
| 26 | 25 | eqcomd 2743 | . . . . 5
⊢ (ℎ = (𝑥 ∈ 𝐴 ↦ 𝑔) → (𝑆‘(𝑥 ∈ 𝐴 ↦ 𝑔)) = (𝑆‘ℎ)) | 
| 27 | 24, 26 | sylan9req 2798 | . . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) ∧ ℎ = (𝑥 ∈ 𝐴 ↦ 𝑔)) → 𝑔 = (𝑆‘ℎ)) | 
| 28 | 12, 27 | rspcedeq2vd 3630 | . . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ∃ℎ ∈ 𝐹 𝑔 = (𝑆‘ℎ)) | 
| 29 | 28 | ralrimiva 3146 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → ∀𝑔 ∈ 𝐵 ∃ℎ ∈ 𝐹 𝑔 = (𝑆‘ℎ)) | 
| 30 |  | dffo3 7122 | . 2
⊢ (𝑆:𝐹–onto→𝐵 ↔ (𝑆:𝐹⟶𝐵 ∧ ∀𝑔 ∈ 𝐵 ∃ℎ ∈ 𝐹 𝑔 = (𝑆‘ℎ))) | 
| 31 | 4, 29, 30 | sylanbrc 583 | 1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → 𝑆:𝐹–onto→𝐵) |