Step |
Hyp |
Ref |
Expression |
1 |
|
fsetfocdm.f |
⊢ 𝐹 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } |
2 |
|
fsetfocdm.s |
⊢ 𝑆 = ( 𝑔 ∈ 𝐹 ↦ ( 𝑔 ‘ 𝑋 ) ) |
3 |
1 2
|
fsetfcdm |
⊢ ( 𝑋 ∈ 𝐴 → 𝑆 : 𝐹 ⟶ 𝐵 ) |
4 |
3
|
adantl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑆 : 𝐹 ⟶ 𝐵 ) |
5 |
|
simplr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑔 ∈ 𝐵 ) |
6 |
5
|
fmpttd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 ) |
7 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝐴 ∈ 𝑉 ) |
8 |
7
|
mptexd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ V ) |
9 |
|
feq1 |
⊢ ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 ) ) |
10 |
9 1
|
elab2g |
⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ V → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ 𝐹 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 ) ) |
11 |
8 10
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ 𝐹 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 ) ) |
12 |
6 11
|
mpbird |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ 𝐹 ) |
13 |
|
fveq1 |
⊢ ( 𝑔 = 𝑓 → ( 𝑔 ‘ 𝑋 ) = ( 𝑓 ‘ 𝑋 ) ) |
14 |
13
|
cbvmptv |
⊢ ( 𝑔 ∈ 𝐹 ↦ ( 𝑔 ‘ 𝑋 ) ) = ( 𝑓 ∈ 𝐹 ↦ ( 𝑓 ‘ 𝑋 ) ) |
15 |
2 14
|
eqtri |
⊢ 𝑆 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑓 ‘ 𝑋 ) ) |
16 |
|
fveq1 |
⊢ ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑓 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) ) |
17 |
|
fvexd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) ∈ V ) |
18 |
15 16 12 17
|
fvmptd3 |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) ) |
19 |
|
eqidd |
⊢ ( 𝑥 = 𝑋 → 𝑔 = 𝑔 ) |
20 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) |
21 |
|
vex |
⊢ 𝑔 ∈ V |
22 |
19 20 21
|
fvmpt |
⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) = 𝑔 ) |
23 |
22
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) = 𝑔 ) |
24 |
18 23
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) = 𝑔 ) |
25 |
|
fveq2 |
⊢ ( ℎ = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑆 ‘ ℎ ) = ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) ) |
26 |
25
|
eqcomd |
⊢ ( ℎ = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) = ( 𝑆 ‘ ℎ ) ) |
27 |
24 26
|
sylan9req |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) → 𝑔 = ( 𝑆 ‘ ℎ ) ) |
28 |
12 27
|
rspcedeq2vd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ∃ ℎ ∈ 𝐹 𝑔 = ( 𝑆 ‘ ℎ ) ) |
29 |
28
|
ralrimiva |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑔 ∈ 𝐵 ∃ ℎ ∈ 𝐹 𝑔 = ( 𝑆 ‘ ℎ ) ) |
30 |
|
dffo3 |
⊢ ( 𝑆 : 𝐹 –onto→ 𝐵 ↔ ( 𝑆 : 𝐹 ⟶ 𝐵 ∧ ∀ 𝑔 ∈ 𝐵 ∃ ℎ ∈ 𝐹 𝑔 = ( 𝑆 ‘ ℎ ) ) ) |
31 |
4 29 30
|
sylanbrc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑆 : 𝐹 –onto→ 𝐵 ) |