Step | Hyp | Ref
| Expression |
1 | | fsetsnf.a |
. . 3
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}} |
2 | | fsetsnf.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩}) |
3 | 1, 2 | fsetsnf 45761 |
. 2
⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵⟶𝐴) |
4 | | vex 3479 |
. . . . . 6
⊢ 𝑚 ∈ V |
5 | | eqeq1 2737 |
. . . . . . 7
⊢ (𝑦 = 𝑚 → (𝑦 = {⟨𝑆, 𝑏⟩} ↔ 𝑚 = {⟨𝑆, 𝑏⟩})) |
6 | 5 | rexbidv 3179 |
. . . . . 6
⊢ (𝑦 = 𝑚 → (∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩} ↔ ∃𝑏 ∈ 𝐵 𝑚 = {⟨𝑆, 𝑏⟩})) |
7 | 4, 6, 1 | elab2 3673 |
. . . . 5
⊢ (𝑚 ∈ 𝐴 ↔ ∃𝑏 ∈ 𝐵 𝑚 = {⟨𝑆, 𝑏⟩}) |
8 | | opeq2 4875 |
. . . . . . . . 9
⊢ (𝑏 = 𝑛 → ⟨𝑆, 𝑏⟩ = ⟨𝑆, 𝑛⟩) |
9 | 8 | sneqd 4641 |
. . . . . . . 8
⊢ (𝑏 = 𝑛 → {⟨𝑆, 𝑏⟩} = {⟨𝑆, 𝑛⟩}) |
10 | 9 | eqeq2d 2744 |
. . . . . . 7
⊢ (𝑏 = 𝑛 → (𝑚 = {⟨𝑆, 𝑏⟩} ↔ 𝑚 = {⟨𝑆, 𝑛⟩})) |
11 | 10 | cbvrexvw 3236 |
. . . . . 6
⊢
(∃𝑏 ∈
𝐵 𝑚 = {⟨𝑆, 𝑏⟩} ↔ ∃𝑛 ∈ 𝐵 𝑚 = {⟨𝑆, 𝑛⟩}) |
12 | | simpr 486 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) ∧ 𝑚 = {⟨𝑆, 𝑛⟩}) → 𝑚 = {⟨𝑆, 𝑛⟩}) |
13 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩})) |
14 | | opeq2 4875 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑛 → ⟨𝑆, 𝑥⟩ = ⟨𝑆, 𝑛⟩) |
15 | 14 | sneqd 4641 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑛 → {⟨𝑆, 𝑥⟩} = {⟨𝑆, 𝑛⟩}) |
16 | 15 | adantl 483 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) ∧ 𝑥 = 𝑛) → {⟨𝑆, 𝑥⟩} = {⟨𝑆, 𝑛⟩}) |
17 | | simpr 486 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ 𝐵) |
18 | | snex 5432 |
. . . . . . . . . . . . 13
⊢
{⟨𝑆, 𝑛⟩} ∈
V |
19 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → {⟨𝑆, 𝑛⟩} ∈ V) |
20 | 13, 16, 17, 19 | fvmptd 7006 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) = {⟨𝑆, 𝑛⟩}) |
21 | 20 | eqcomd 2739 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → {⟨𝑆, 𝑛⟩} = (𝐹‘𝑛)) |
22 | 21 | adantr 482 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) ∧ 𝑚 = {⟨𝑆, 𝑛⟩}) → {⟨𝑆, 𝑛⟩} = (𝐹‘𝑛)) |
23 | 12, 22 | eqtrd 2773 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) ∧ 𝑚 = {⟨𝑆, 𝑛⟩}) → 𝑚 = (𝐹‘𝑛)) |
24 | 23 | ex 414 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵) → (𝑚 = {⟨𝑆, 𝑛⟩} → 𝑚 = (𝐹‘𝑛))) |
25 | 24 | reximdva 3169 |
. . . . . 6
⊢ (𝑆 ∈ 𝑉 → (∃𝑛 ∈ 𝐵 𝑚 = {⟨𝑆, 𝑛⟩} → ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛))) |
26 | 11, 25 | biimtrid 241 |
. . . . 5
⊢ (𝑆 ∈ 𝑉 → (∃𝑏 ∈ 𝐵 𝑚 = {⟨𝑆, 𝑏⟩} → ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛))) |
27 | 7, 26 | biimtrid 241 |
. . . 4
⊢ (𝑆 ∈ 𝑉 → (𝑚 ∈ 𝐴 → ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛))) |
28 | 27 | imp 408 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑚 ∈ 𝐴) → ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛)) |
29 | 28 | ralrimiva 3147 |
. 2
⊢ (𝑆 ∈ 𝑉 → ∀𝑚 ∈ 𝐴 ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛)) |
30 | | dffo3 7104 |
. 2
⊢ (𝐹:𝐵–onto→𝐴 ↔ (𝐹:𝐵⟶𝐴 ∧ ∀𝑚 ∈ 𝐴 ∃𝑛 ∈ 𝐵 𝑚 = (𝐹‘𝑛))) |
31 | 3, 29, 30 | sylanbrc 584 |
1
⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–onto→𝐴) |