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	⊢ 𝐸 Fn V
	slotresfo.v	⊢ ( 𝑘 ∈ 𝐴 → ( 𝐸 ‘ 𝑘 ) ∈ 𝑉 )
	slotresfo.k	⊢ ( 𝑏 ∈ 𝑉 → 𝐾 ∈ 𝐴 )
	slotresfo.b	⊢ ( 𝑏 ∈ 𝑉 → 𝑏 = ( 𝐸 ‘ 𝐾 ) )
Assertion	slotresfo	⊢ ( 𝐸 ↾ 𝐴 ) : 𝐴 –onto→ 𝑉

Proof

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

Metamath Proof Explorer

Theorem slotresfo

Proof