Step | Hyp | Ref
| Expression |
1 | | fsetfocdm.f |
. . . 4
⊢ 𝐹 = {𝑓 ∣ 𝑓:𝐴⟶𝐵} |
2 | | fsetfocdm.s |
. . . 4
⊢ 𝑆 = (𝑔 ∈ 𝐹 ↦ (𝑔‘𝑋)) |
3 | 1, 2 | fsetfcdm 8550 |
. . 3
⊢ (𝑋 ∈ 𝐴 → 𝑆:𝐹⟶𝐵) |
4 | 3 | adantl 485 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → 𝑆:𝐹⟶𝐵) |
5 | | simplr 769 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑔 ∈ 𝐵) |
6 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ 𝑔) = (𝑥 ∈ 𝐴 ↦ 𝑔) |
7 | 5, 6 | fmptd 6940 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝑔):𝐴⟶𝐵) |
8 | | simpll 767 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → 𝐴 ∈ 𝑉) |
9 | 8 | mptexd 7049 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝑔) ∈ V) |
10 | | feq1 6535 |
. . . . . . 7
⊢ (𝑓 = (𝑥 ∈ 𝐴 ↦ 𝑔) → (𝑓:𝐴⟶𝐵 ↔ (𝑥 ∈ 𝐴 ↦ 𝑔):𝐴⟶𝐵)) |
11 | 10, 1 | elab2g 3596 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ↦ 𝑔) ∈ V → ((𝑥 ∈ 𝐴 ↦ 𝑔) ∈ 𝐹 ↔ (𝑥 ∈ 𝐴 ↦ 𝑔):𝐴⟶𝐵)) |
12 | 9, 11 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑔) ∈ 𝐹 ↔ (𝑥 ∈ 𝐴 ↦ 𝑔):𝐴⟶𝐵)) |
13 | 7, 12 | mpbird 260 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝑔) ∈ 𝐹) |
14 | | fveq2 6726 |
. . . . . 6
⊢ (ℎ = (𝑥 ∈ 𝐴 ↦ 𝑔) → (𝑆‘ℎ) = (𝑆‘(𝑥 ∈ 𝐴 ↦ 𝑔))) |
15 | 14 | eqeq2d 2749 |
. . . . 5
⊢ (ℎ = (𝑥 ∈ 𝐴 ↦ 𝑔) → (𝑔 = (𝑆‘ℎ) ↔ 𝑔 = (𝑆‘(𝑥 ∈ 𝐴 ↦ 𝑔)))) |
16 | 15 | adantl 485 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) ∧ ℎ = (𝑥 ∈ 𝐴 ↦ 𝑔)) → (𝑔 = (𝑆‘ℎ) ↔ 𝑔 = (𝑆‘(𝑥 ∈ 𝐴 ↦ 𝑔)))) |
17 | | fveq1 6725 |
. . . . . . . . 9
⊢ (𝑔 = 𝑓 → (𝑔‘𝑋) = (𝑓‘𝑋)) |
18 | 17 | cbvmptv 5167 |
. . . . . . . 8
⊢ (𝑔 ∈ 𝐹 ↦ (𝑔‘𝑋)) = (𝑓 ∈ 𝐹 ↦ (𝑓‘𝑋)) |
19 | 2, 18 | eqtri 2766 |
. . . . . . 7
⊢ 𝑆 = (𝑓 ∈ 𝐹 ↦ (𝑓‘𝑋)) |
20 | 19 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → 𝑆 = (𝑓 ∈ 𝐹 ↦ (𝑓‘𝑋))) |
21 | | fveq1 6725 |
. . . . . . 7
⊢ (𝑓 = (𝑥 ∈ 𝐴 ↦ 𝑔) → (𝑓‘𝑋) = ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋)) |
22 | 21 | adantl 485 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) ∧ 𝑓 = (𝑥 ∈ 𝐴 ↦ 𝑔)) → (𝑓‘𝑋) = ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋)) |
23 | | fvexd 6741 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋) ∈ V) |
24 | 20, 22, 13, 23 | fvmptd 6834 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → (𝑆‘(𝑥 ∈ 𝐴 ↦ 𝑔)) = ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋)) |
25 | | eqidd 2739 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↦ 𝑔) = (𝑥 ∈ 𝐴 ↦ 𝑔)) |
26 | | eqidd 2739 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 = 𝑋) → 𝑔 = 𝑔) |
27 | | simpr 488 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴) |
28 | | vex 3419 |
. . . . . . . 8
⊢ 𝑔 ∈ V |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → 𝑔 ∈ V) |
30 | 25, 26, 27, 29 | fvmptd 6834 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋) = 𝑔) |
31 | 30 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑔)‘𝑋) = 𝑔) |
32 | 24, 31 | eqtr2d 2779 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → 𝑔 = (𝑆‘(𝑥 ∈ 𝐴 ↦ 𝑔))) |
33 | 13, 16, 32 | rspcedvd 3547 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) ∧ 𝑔 ∈ 𝐵) → ∃ℎ ∈ 𝐹 𝑔 = (𝑆‘ℎ)) |
34 | 33 | ralrimiva 3106 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → ∀𝑔 ∈ 𝐵 ∃ℎ ∈ 𝐹 𝑔 = (𝑆‘ℎ)) |
35 | | dffo3 6930 |
. 2
⊢ (𝑆:𝐹–onto→𝐵 ↔ (𝑆:𝐹⟶𝐵 ∧ ∀𝑔 ∈ 𝐵 ∃ℎ ∈ 𝐹 𝑔 = (𝑆‘ℎ))) |
36 | 4, 34, 35 | sylanbrc 586 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → 𝑆:𝐹–onto→𝐵) |