Metamath Proof Explorer

Theorem slotresfo

Description: The condition of a structure component extractor restricted to a class being a surjection. This combined with fonex can be used to prove a class being proper. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses slotresfo.e ⊢ E Fn V
slotresfo.v ⊢ k ∈ A → E ⁡ k ∈ V
slotresfo.k ⊢ b ∈ V → K ∈ A
slotresfo.b ⊢ b ∈ V → b = E ⁡ K
Assertion slotresfo ⊢ E ↾ A : A ⟶ onto V

Proof

Step Hyp Ref Expression
1 slotresfo.e ⊢ E Fn V
2 slotresfo.v ⊢ k ∈ A → E ⁡ k ∈ V
3 slotresfo.k ⊢ b ∈ V → K ∈ A
4 slotresfo.b ⊢ b ∈ V → b = E ⁡ K
5 ssv ⊢ A ⊆ V
6 fnssres ⊢ E Fn V ∧ A ⊆ V → E ↾ A Fn A
7 1 5 6 mp2an ⊢ E ↾ A Fn A
8 fvres ⊢ k ∈ A → E ↾ A ⁡ k = E ⁡ k
9 8 2 eqeltrd ⊢ k ∈ A → E ↾ A ⁡ k ∈ V
10 9 rgen ⊢ ∀ k ∈ A E ↾ A ⁡ k ∈ V
11 fnfvrnss ⊢ E ↾ A Fn A ∧ ∀ k ∈ A E ↾ A ⁡ k ∈ V → ran ⁡ E ↾ A ⊆ V
12 7 10 11 mp2an ⊢ ran ⁡ E ↾ A ⊆ V
13 df-f ⊢ E ↾ A : A ⟶ V ↔ E ↾ A Fn A ∧ ran ⁡ E ↾ A ⊆ V
14 7 12 13 mpbir2an ⊢ E ↾ A : A ⟶ V
15 fveq2 ⊢ k = K → E ⁡ k = E ⁡ K
16 15 eqeq2d ⊢ k = K → b = E ⁡ k ↔ b = E ⁡ K
17 16 3 4 rspcedvdw ⊢ b ∈ V → ∃ k ∈ A b = E ⁡ k
18 8 eqeq2d ⊢ k ∈ A → b = E ↾ A ⁡ k ↔ b = E ⁡ k
19 18 rexbiia ⊢ ∃ k ∈ A b = E ↾ A ⁡ k ↔ ∃ k ∈ A b = E ⁡ k
20 17 19 sylibr ⊢ b ∈ V → ∃ k ∈ A b = E ↾ A ⁡ k
21 20 rgen ⊢ ∀ b ∈ V ∃ k ∈ A b = E ↾ A ⁡ k
22 dffo3 ⊢ E ↾ A : A ⟶ onto V ↔ E ↾ A : A ⟶ V ∧ ∀ b ∈ V ∃ k ∈ A b = E ↾ A ⁡ k
23 14 21 22 mpbir2an ⊢ E ↾ A : A ⟶ onto V