| Step | Hyp | Ref
| Expression |
| 1 | | fsn2g 7158 |
. . . . . 6
⊢ (𝑆 ∈ 𝑉 → (𝑔:{𝑆}⟶𝐵 ↔ ((𝑔‘𝑆) ∈ 𝐵 ∧ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}))) |
| 2 | | simpl 482 |
. . . . . . 7
⊢ (((𝑔‘𝑆) ∈ 𝐵 ∧ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}) → (𝑔‘𝑆) ∈ 𝐵) |
| 3 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑔‘𝑆) → 〈𝑆, 𝑏〉 = 〈𝑆, (𝑔‘𝑆)〉) |
| 4 | 3 | sneqd 4638 |
. . . . . . . . 9
⊢ (𝑏 = (𝑔‘𝑆) → {〈𝑆, 𝑏〉} = {〈𝑆, (𝑔‘𝑆)〉}) |
| 5 | 4 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑏 = (𝑔‘𝑆) → (𝑔 = {〈𝑆, 𝑏〉} ↔ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉})) |
| 6 | 5 | adantl 481 |
. . . . . . 7
⊢ ((((𝑔‘𝑆) ∈ 𝐵 ∧ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}) ∧ 𝑏 = (𝑔‘𝑆)) → (𝑔 = {〈𝑆, 𝑏〉} ↔ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉})) |
| 7 | | simpr 484 |
. . . . . . 7
⊢ (((𝑔‘𝑆) ∈ 𝐵 ∧ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}) → 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}) |
| 8 | 2, 6, 7 | rspcedvd 3624 |
. . . . . 6
⊢ (((𝑔‘𝑆) ∈ 𝐵 ∧ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}) → ∃𝑏 ∈ 𝐵 𝑔 = {〈𝑆, 𝑏〉}) |
| 9 | 1, 8 | biimtrdi 253 |
. . . . 5
⊢ (𝑆 ∈ 𝑉 → (𝑔:{𝑆}⟶𝐵 → ∃𝑏 ∈ 𝐵 𝑔 = {〈𝑆, 𝑏〉})) |
| 10 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) → 𝑆 ∈ 𝑉) |
| 11 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
| 12 | 10, 11 | fsnd 6891 |
. . . . . . . . 9
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) → {〈𝑆, 𝑏〉}:{𝑆}⟶𝐵) |
| 13 | 12 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) ∧ 𝑔 = {〈𝑆, 𝑏〉}) → {〈𝑆, 𝑏〉}:{𝑆}⟶𝐵) |
| 14 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) ∧ 𝑔 = {〈𝑆, 𝑏〉}) → 𝑔 = {〈𝑆, 𝑏〉}) |
| 15 | 14 | feq1d 6720 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) ∧ 𝑔 = {〈𝑆, 𝑏〉}) → (𝑔:{𝑆}⟶𝐵 ↔ {〈𝑆, 𝑏〉}:{𝑆}⟶𝐵)) |
| 16 | 13, 15 | mpbird 257 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) ∧ 𝑔 = {〈𝑆, 𝑏〉}) → 𝑔:{𝑆}⟶𝐵) |
| 17 | 16 | ex 412 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) → (𝑔 = {〈𝑆, 𝑏〉} → 𝑔:{𝑆}⟶𝐵)) |
| 18 | 17 | rexlimdva 3155 |
. . . . 5
⊢ (𝑆 ∈ 𝑉 → (∃𝑏 ∈ 𝐵 𝑔 = {〈𝑆, 𝑏〉} → 𝑔:{𝑆}⟶𝐵)) |
| 19 | 9, 18 | impbid 212 |
. . . 4
⊢ (𝑆 ∈ 𝑉 → (𝑔:{𝑆}⟶𝐵 ↔ ∃𝑏 ∈ 𝐵 𝑔 = {〈𝑆, 𝑏〉})) |
| 20 | | velsn 4642 |
. . . . . 6
⊢ (𝑔 ∈ {{〈𝑆, 𝑏〉}} ↔ 𝑔 = {〈𝑆, 𝑏〉}) |
| 21 | 20 | bicomi 224 |
. . . . 5
⊢ (𝑔 = {〈𝑆, 𝑏〉} ↔ 𝑔 ∈ {{〈𝑆, 𝑏〉}}) |
| 22 | 21 | rexbii 3094 |
. . . 4
⊢
(∃𝑏 ∈
𝐵 𝑔 = {〈𝑆, 𝑏〉} ↔ ∃𝑏 ∈ 𝐵 𝑔 ∈ {{〈𝑆, 𝑏〉}}) |
| 23 | 19, 22 | bitrdi 287 |
. . 3
⊢ (𝑆 ∈ 𝑉 → (𝑔:{𝑆}⟶𝐵 ↔ ∃𝑏 ∈ 𝐵 𝑔 ∈ {{〈𝑆, 𝑏〉}})) |
| 24 | | vex 3484 |
. . . 4
⊢ 𝑔 ∈ V |
| 25 | | feq1 6716 |
. . . 4
⊢ (𝑓 = 𝑔 → (𝑓:{𝑆}⟶𝐵 ↔ 𝑔:{𝑆}⟶𝐵)) |
| 26 | 24, 25 | elab 3679 |
. . 3
⊢ (𝑔 ∈ {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} ↔ 𝑔:{𝑆}⟶𝐵) |
| 27 | | eliun 4995 |
. . 3
⊢ (𝑔 ∈ ∪ 𝑏 ∈ 𝐵 {{〈𝑆, 𝑏〉}} ↔ ∃𝑏 ∈ 𝐵 𝑔 ∈ {{〈𝑆, 𝑏〉}}) |
| 28 | 23, 26, 27 | 3bitr4g 314 |
. 2
⊢ (𝑆 ∈ 𝑉 → (𝑔 ∈ {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} ↔ 𝑔 ∈ ∪
𝑏 ∈ 𝐵 {{〈𝑆, 𝑏〉}})) |
| 29 | 28 | eqrdv 2735 |
1
⊢ (𝑆 ∈ 𝑉 → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} = ∪
𝑏 ∈ 𝐵 {{〈𝑆, 𝑏〉}}) |