| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fsetsnf.a | . . 3
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {〈𝑆, 𝑏〉}} | 
| 2 |  | fsetsnf.f | . . 3
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {〈𝑆, 𝑥〉}) | 
| 3 | 1, 2 | fsetsnf 47068 | . 2
⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵⟶𝐴) | 
| 4 |  | vex 3483 | . . . . . 6
⊢ 𝑚 ∈ V | 
| 5 |  | eqeq1 2740 | . . . . . . 7
⊢ (𝑦 = 𝑚 → (𝑦 = {〈𝑆, 𝑏〉} ↔ 𝑚 = {〈𝑆, 𝑏〉})) | 
| 6 | 5 | rexbidv 3178 | . . . . . 6
⊢ (𝑦 = 𝑚 → (∃𝑏 ∈ 𝐵 𝑦 = {〈𝑆, 𝑏〉} ↔ ∃𝑏 ∈ 𝐵 𝑚 = {〈𝑆, 𝑏〉})) | 
| 7 | 4, 6, 1 | elab2 3681 | . . . . 5
⊢ (𝑚 ∈ 𝐴 ↔ ∃𝑏 ∈ 𝐵 𝑚 = {〈𝑆, 𝑏〉}) | 
| 8 |  | opeq2 4873 | . . . . . . . . 9
⊢ (𝑏 = 𝑛 → 〈𝑆, 𝑏〉 = 〈𝑆, 𝑛〉) | 
| 9 | 8 | sneqd 4637 | . . . . . . . 8
⊢ (𝑏 = 𝑛 → {〈𝑆, 𝑏〉} = {〈𝑆, 𝑛〉}) | 
| 10 | 9 | eqeq2d 2747 | . . . . . . 7
⊢ (𝑏 = 𝑛 → (𝑚 = {〈𝑆, 𝑏〉} ↔ 𝑚 = {〈𝑆, 𝑛〉})) | 
| 11 | 10 | cbvrexvw 3237 | . . . . . 6
⊢
(∃𝑏 ∈
𝐵 𝑚 = {〈𝑆, 𝑏〉} ↔ ∃𝑛 ∈ 𝐵 𝑚 = {〈𝑆, 𝑛〉}) | 
| 12 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) ∧ 𝑚 = {〈𝑆, 𝑛〉}) → 𝑚 = {〈𝑆, 𝑛〉}) | 
| 13 | 2 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → 𝐹 = (𝑥 ∈ 𝐵 ↦ {〈𝑆, 𝑥〉})) | 
| 14 |  | opeq2 4873 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑛 → 〈𝑆, 𝑥〉 = 〈𝑆, 𝑛〉) | 
| 15 | 14 | sneqd 4637 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑛 → {〈𝑆, 𝑥〉} = {〈𝑆, 𝑛〉}) | 
| 16 | 15 | adantl 481 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) ∧ 𝑥 = 𝑛) → {〈𝑆, 𝑥〉} = {〈𝑆, 𝑛〉}) | 
| 17 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ 𝐵) | 
| 18 |  | snex 5435 | . . . . . . . . . . . . 13
⊢
{〈𝑆, 𝑛〉} ∈
V | 
| 19 | 18 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → {〈𝑆, 𝑛〉} ∈ V) | 
| 20 | 13, 16, 17, 19 | fvmptd 7022 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) = {〈𝑆, 𝑛〉}) | 
| 21 | 20 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → {〈𝑆, 𝑛〉} = (𝐹‘𝑛)) | 
| 22 | 21 | adantr 480 | . . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) ∧ 𝑚 = {〈𝑆, 𝑛〉}) → {〈𝑆, 𝑛〉} = (𝐹‘𝑛)) | 
| 23 | 12, 22 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) ∧ 𝑚 = {〈𝑆, 𝑛〉}) → 𝑚 = (𝐹‘𝑛)) | 
| 24 | 23 | ex 412 | . . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → (𝑚 = {〈𝑆, 𝑛〉} → 𝑚 = (𝐹‘𝑛))) | 
| 25 | 24 | reximdva 3167 | . . . . . 6
⊢ (𝑆 ∈ 𝑉 → (∃𝑛 ∈ 𝐵 𝑚 = {〈𝑆, 𝑛〉} → ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛))) | 
| 26 | 11, 25 | biimtrid 242 | . . . . 5
⊢ (𝑆 ∈ 𝑉 → (∃𝑏 ∈ 𝐵 𝑚 = {〈𝑆, 𝑏〉} → ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛))) | 
| 27 | 7, 26 | biimtrid 242 | . . . 4
⊢ (𝑆 ∈ 𝑉 → (𝑚 ∈ 𝐴 → ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛))) | 
| 28 | 27 | imp 406 | . . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑚 ∈ 𝐴) → ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛)) | 
| 29 | 28 | ralrimiva 3145 | . 2
⊢ (𝑆 ∈ 𝑉 → ∀𝑚 ∈ 𝐴 ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛)) | 
| 30 |  | dffo3 7121 | . 2
⊢ (𝐹:𝐵–onto→𝐴 ↔ (𝐹:𝐵⟶𝐴 ∧ ∀𝑚 ∈ 𝐴 ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛))) | 
| 31 | 3, 29, 30 | sylanbrc 583 | 1
⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–onto→𝐴) |