Step |
Hyp |
Ref |
Expression |
1 |
|
f11o.1 |
⊢ 𝐹 ∈ V |
2 |
|
df-f |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ) |
3 |
|
dffn4 |
⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 ) |
4 |
3
|
anbi1i |
⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ↔ ( 𝐹 : 𝐴 –onto→ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) ) |
5 |
2 4
|
bitri |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 : 𝐴 –onto→ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) ) |
6 |
1
|
rnex |
⊢ ran 𝐹 ∈ V |
7 |
|
foeq3 |
⊢ ( 𝑥 = ran 𝐹 → ( 𝐹 : 𝐴 –onto→ 𝑥 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 ) ) |
8 |
|
sseq1 |
⊢ ( 𝑥 = ran 𝐹 → ( 𝑥 ⊆ 𝐵 ↔ ran 𝐹 ⊆ 𝐵 ) ) |
9 |
7 8
|
anbi12d |
⊢ ( 𝑥 = ran 𝐹 → ( ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐹 : 𝐴 –onto→ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) ) ) |
10 |
6 9
|
spcev |
⊢ ( ( 𝐹 : 𝐴 –onto→ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) |
11 |
5 10
|
sylbi |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) |
12 |
|
fof |
⊢ ( 𝐹 : 𝐴 –onto→ 𝑥 → 𝐹 : 𝐴 ⟶ 𝑥 ) |
13 |
|
fss |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
14 |
12 13
|
sylan |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
15 |
14
|
exlimiv |
⊢ ( ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
16 |
11 15
|
impbii |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ∃ 𝑥 ( 𝐹 : 𝐴 –onto→ 𝑥 ∧ 𝑥 ⊆ 𝐵 ) ) |