Step | Hyp | Ref
| Expression |
1 | | fsetsnf.a |
. . 3
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}} |
2 | | fsetsnf.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩}) |
3 | 1, 2 | fsetsnf 45761 |
. 2
⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵⟶𝐴) |
4 | 2 | a1i 11 |
. . . . . . 7
⊢ ((𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) → 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩})) |
5 | | opeq2 4875 |
. . . . . . . . 9
⊢ (𝑥 = 𝑚 → ⟨𝑆, 𝑥⟩ = ⟨𝑆, 𝑚⟩) |
6 | 5 | sneqd 4641 |
. . . . . . . 8
⊢ (𝑥 = 𝑚 → {⟨𝑆, 𝑥⟩} = {⟨𝑆, 𝑚⟩}) |
7 | 6 | adantl 483 |
. . . . . . 7
⊢ (((𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) ∧ 𝑥 = 𝑚) → {⟨𝑆, 𝑥⟩} = {⟨𝑆, 𝑚⟩}) |
8 | | simpl 484 |
. . . . . . 7
⊢ ((𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) → 𝑚 ∈ 𝐵) |
9 | | snex 5432 |
. . . . . . . 8
⊢
{⟨𝑆, 𝑚⟩} ∈
V |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ ((𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) → {⟨𝑆, 𝑚⟩} ∈ V) |
11 | 4, 7, 8, 10 | fvmptd 7006 |
. . . . . 6
⊢ ((𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑚) = {⟨𝑆, 𝑚⟩}) |
12 | | opeq2 4875 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → ⟨𝑆, 𝑥⟩ = ⟨𝑆, 𝑛⟩) |
13 | 12 | sneqd 4641 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → {⟨𝑆, 𝑥⟩} = {⟨𝑆, 𝑛⟩}) |
14 | 13 | adantl 483 |
. . . . . . 7
⊢ (((𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) ∧ 𝑥 = 𝑛) → {⟨𝑆, 𝑥⟩} = {⟨𝑆, 𝑛⟩}) |
15 | | simpr 486 |
. . . . . . 7
⊢ ((𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) → 𝑛 ∈ 𝐵) |
16 | | snex 5432 |
. . . . . . . 8
⊢
{⟨𝑆, 𝑛⟩} ∈
V |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ ((𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) → {⟨𝑆, 𝑛⟩} ∈ V) |
18 | 4, 14, 15, 17 | fvmptd 7006 |
. . . . . 6
⊢ ((𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) → (𝐹‘𝑛) = {⟨𝑆, 𝑛⟩}) |
19 | 11, 18 | eqeq12d 2749 |
. . . . 5
⊢ ((𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵) → ((𝐹‘𝑚) = (𝐹‘𝑛) ↔ {⟨𝑆, 𝑚⟩} = {⟨𝑆, 𝑛⟩})) |
20 | 19 | adantl 483 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ (𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵)) → ((𝐹‘𝑚) = (𝐹‘𝑛) ↔ {⟨𝑆, 𝑚⟩} = {⟨𝑆, 𝑛⟩})) |
21 | | opex 5465 |
. . . . . 6
⊢
⟨𝑆, 𝑚⟩ ∈ V |
22 | 21 | sneqr 4842 |
. . . . 5
⊢
({⟨𝑆, 𝑚⟩} = {⟨𝑆, 𝑛⟩} → ⟨𝑆, 𝑚⟩ = ⟨𝑆, 𝑛⟩) |
23 | | opthg 5478 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑚 ∈ 𝐵) → (⟨𝑆, 𝑚⟩ = ⟨𝑆, 𝑛⟩ ↔ (𝑆 = 𝑆 ∧ 𝑚 = 𝑛))) |
24 | 23 | adantrr 716 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ (𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵)) → (⟨𝑆, 𝑚⟩ = ⟨𝑆, 𝑛⟩ ↔ (𝑆 = 𝑆 ∧ 𝑚 = 𝑛))) |
25 | | simpr 486 |
. . . . . 6
⊢ ((𝑆 = 𝑆 ∧ 𝑚 = 𝑛) → 𝑚 = 𝑛) |
26 | 24, 25 | syl6bi 253 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ (𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵)) → (⟨𝑆, 𝑚⟩ = ⟨𝑆, 𝑛⟩ → 𝑚 = 𝑛)) |
27 | 22, 26 | syl5 34 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ (𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵)) → ({⟨𝑆, 𝑚⟩} = {⟨𝑆, 𝑛⟩} → 𝑚 = 𝑛)) |
28 | 20, 27 | sylbid 239 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ (𝑚 ∈ 𝐵 ∧ 𝑛 ∈ 𝐵)) → ((𝐹‘𝑚) = (𝐹‘𝑛) → 𝑚 = 𝑛)) |
29 | 28 | ralrimivva 3201 |
. 2
⊢ (𝑆 ∈ 𝑉 → ∀𝑚 ∈ 𝐵 ∀𝑛 ∈ 𝐵 ((𝐹‘𝑚) = (𝐹‘𝑛) → 𝑚 = 𝑛)) |
30 | | dff13 7254 |
. 2
⊢ (𝐹:𝐵–1-1→𝐴 ↔ (𝐹:𝐵⟶𝐴 ∧ ∀𝑚 ∈ 𝐵 ∀𝑛 ∈ 𝐵 ((𝐹‘𝑚) = (𝐹‘𝑛) → 𝑚 = 𝑛))) |
31 | 3, 29, 30 | sylanbrc 584 |
1
⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵–1-1→𝐴) |