Step | Hyp | Ref
| Expression |
1 | | fsn2g 6972 |
. . . . . 6
⊢ (𝑆 ∈ 𝑉 → (𝑔:{𝑆}⟶𝐵 ↔ ((𝑔‘𝑆) ∈ 𝐵 ∧ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}))) |
2 | | simpl 486 |
. . . . . . 7
⊢ (((𝑔‘𝑆) ∈ 𝐵 ∧ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}) → (𝑔‘𝑆) ∈ 𝐵) |
3 | | opeq2 4800 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑔‘𝑆) → 〈𝑆, 𝑏〉 = 〈𝑆, (𝑔‘𝑆)〉) |
4 | 3 | sneqd 4568 |
. . . . . . . . 9
⊢ (𝑏 = (𝑔‘𝑆) → {〈𝑆, 𝑏〉} = {〈𝑆, (𝑔‘𝑆)〉}) |
5 | 4 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑏 = (𝑔‘𝑆) → (𝑔 = {〈𝑆, 𝑏〉} ↔ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉})) |
6 | 5 | adantl 485 |
. . . . . . 7
⊢ ((((𝑔‘𝑆) ∈ 𝐵 ∧ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}) ∧ 𝑏 = (𝑔‘𝑆)) → (𝑔 = {〈𝑆, 𝑏〉} ↔ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉})) |
7 | | simpr 488 |
. . . . . . 7
⊢ (((𝑔‘𝑆) ∈ 𝐵 ∧ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}) → 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}) |
8 | 2, 6, 7 | rspcedvd 3553 |
. . . . . 6
⊢ (((𝑔‘𝑆) ∈ 𝐵 ∧ 𝑔 = {〈𝑆, (𝑔‘𝑆)〉}) → ∃𝑏 ∈ 𝐵 𝑔 = {〈𝑆, 𝑏〉}) |
9 | 1, 8 | syl6bi 256 |
. . . . 5
⊢ (𝑆 ∈ 𝑉 → (𝑔:{𝑆}⟶𝐵 → ∃𝑏 ∈ 𝐵 𝑔 = {〈𝑆, 𝑏〉})) |
10 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) → 𝑆 ∈ 𝑉) |
11 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
12 | 10, 11 | fsnd 6722 |
. . . . . . . . 9
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) → {〈𝑆, 𝑏〉}:{𝑆}⟶𝐵) |
13 | 12 | adantr 484 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) ∧ 𝑔 = {〈𝑆, 𝑏〉}) → {〈𝑆, 𝑏〉}:{𝑆}⟶𝐵) |
14 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) ∧ 𝑔 = {〈𝑆, 𝑏〉}) → 𝑔 = {〈𝑆, 𝑏〉}) |
15 | 14 | feq1d 6549 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) ∧ 𝑔 = {〈𝑆, 𝑏〉}) → (𝑔:{𝑆}⟶𝐵 ↔ {〈𝑆, 𝑏〉}:{𝑆}⟶𝐵)) |
16 | 13, 15 | mpbird 260 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) ∧ 𝑔 = {〈𝑆, 𝑏〉}) → 𝑔:{𝑆}⟶𝐵) |
17 | 16 | ex 416 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) → (𝑔 = {〈𝑆, 𝑏〉} → 𝑔:{𝑆}⟶𝐵)) |
18 | 17 | rexlimdva 3211 |
. . . . 5
⊢ (𝑆 ∈ 𝑉 → (∃𝑏 ∈ 𝐵 𝑔 = {〈𝑆, 𝑏〉} → 𝑔:{𝑆}⟶𝐵)) |
19 | 9, 18 | impbid 215 |
. . . 4
⊢ (𝑆 ∈ 𝑉 → (𝑔:{𝑆}⟶𝐵 ↔ ∃𝑏 ∈ 𝐵 𝑔 = {〈𝑆, 𝑏〉})) |
20 | | velsn 4572 |
. . . . . 6
⊢ (𝑔 ∈ {{〈𝑆, 𝑏〉}} ↔ 𝑔 = {〈𝑆, 𝑏〉}) |
21 | 20 | bicomi 227 |
. . . . 5
⊢ (𝑔 = {〈𝑆, 𝑏〉} ↔ 𝑔 ∈ {{〈𝑆, 𝑏〉}}) |
22 | 21 | rexbii 3176 |
. . . 4
⊢
(∃𝑏 ∈
𝐵 𝑔 = {〈𝑆, 𝑏〉} ↔ ∃𝑏 ∈ 𝐵 𝑔 ∈ {{〈𝑆, 𝑏〉}}) |
23 | 19, 22 | bitrdi 290 |
. . 3
⊢ (𝑆 ∈ 𝑉 → (𝑔:{𝑆}⟶𝐵 ↔ ∃𝑏 ∈ 𝐵 𝑔 ∈ {{〈𝑆, 𝑏〉}})) |
24 | | vex 3425 |
. . . 4
⊢ 𝑔 ∈ V |
25 | | feq1 6545 |
. . . 4
⊢ (𝑓 = 𝑔 → (𝑓:{𝑆}⟶𝐵 ↔ 𝑔:{𝑆}⟶𝐵)) |
26 | 24, 25 | elab 3600 |
. . 3
⊢ (𝑔 ∈ {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} ↔ 𝑔:{𝑆}⟶𝐵) |
27 | | eliun 4923 |
. . 3
⊢ (𝑔 ∈ ∪ 𝑏 ∈ 𝐵 {{〈𝑆, 𝑏〉}} ↔ ∃𝑏 ∈ 𝐵 𝑔 ∈ {{〈𝑆, 𝑏〉}}) |
28 | 23, 26, 27 | 3bitr4g 317 |
. 2
⊢ (𝑆 ∈ 𝑉 → (𝑔 ∈ {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} ↔ 𝑔 ∈ ∪
𝑏 ∈ 𝐵 {{〈𝑆, 𝑏〉}})) |
29 | 28 | eqrdv 2736 |
1
⊢ (𝑆 ∈ 𝑉 → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} = ∪
𝑏 ∈ 𝐵 {{〈𝑆, 𝑏〉}}) |