fsetfocdm

Description: The class of functions with a given domain that is a set and a given codomain is mapped, through evaluation at a point of the domain, onto the codomain. (Contributed by AV, 15-Sep-2024)

	Ref	Expression
Hypotheses	fsetfocdm.f	$⊢ F = \{f \| f : A ⟶ B\}$
	fsetfocdm.s	$⊢ S = (g \in F ⟼ g (X))$
Assertion	fsetfocdm	$⊢ (A \in V \land X \in A) \to S : F \underset{onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		fsetfocdm.f	$⊢ F = \{f \| f : A ⟶ B\}$
2		fsetfocdm.s	$⊢ S = (g \in F ⟼ g (X))$
3	1 2	fsetfcdm	$⊢ X \in A \to S : F ⟶ B$
4	3	adantl	$⊢ (A \in V \land X \in A) \to S : F ⟶ B$
5		simplr	$⊢ (((A \in V \land X \in A) \land g \in B) \land x \in A) \to g \in B$
6		eqid	$⊢ (x \in A ⟼ g) = (x \in A ⟼ g)$
7	5 6	fmptd	$⊢ ((A \in V \land X \in A) \land g \in B) \to (x \in A ⟼ g) : A ⟶ B$
8		simpll	$⊢ ((A \in V \land X \in A) \land g \in B) \to A \in V$
9	8	mptexd	$⊢ ((A \in V \land X \in A) \land g \in B) \to (x \in A ⟼ g) \in V$
10		feq1	$⊢ f = (x \in A ⟼ g) \to (f : A ⟶ B \leftrightarrow (x \in A ⟼ g) : A ⟶ B)$
11	10 1	elab2g	$⊢ (x \in A ⟼ g) \in V \to ((x \in A ⟼ g) \in F \leftrightarrow (x \in A ⟼ g) : A ⟶ B)$
12	9 11	syl	$⊢ ((A \in V \land X \in A) \land g \in B) \to ((x \in A ⟼ g) \in F \leftrightarrow (x \in A ⟼ g) : A ⟶ B)$
13	7 12	mpbird	$⊢ ((A \in V \land X \in A) \land g \in B) \to (x \in A ⟼ g) \in F$
14		fveq2	$⊢ h = (x \in A ⟼ g) \to S (h) = S ((x \in A ⟼ g))$
15	14	eqeq2d	$⊢ h = (x \in A ⟼ g) \to (g = S (h) \leftrightarrow g = S ((x \in A ⟼ g)))$
16	15	adantl	$⊢ (((A \in V \land X \in A) \land g \in B) \land h = (x \in A ⟼ g)) \to (g = S (h) \leftrightarrow g = S ((x \in A ⟼ g)))$
17		fveq1	$⊢ g = f \to g (X) = f (X)$
18	17	cbvmptv	$⊢ (g \in F ⟼ g (X)) = (f \in F ⟼ f (X))$
19	2 18	eqtri	$⊢ S = (f \in F ⟼ f (X))$
20	19	a1i	$⊢ ((A \in V \land X \in A) \land g \in B) \to S = (f \in F ⟼ f (X))$
21		fveq1	$⊢ f = (x \in A ⟼ g) \to f (X) = (x \in A ⟼ g) (X)$
22	21	adantl	$⊢ (((A \in V \land X \in A) \land g \in B) \land f = (x \in A ⟼ g)) \to f (X) = (x \in A ⟼ g) (X)$
23		fvexd	$⊢ ((A \in V \land X \in A) \land g \in B) \to (x \in A ⟼ g) (X) \in V$
24	20 22 13 23	fvmptd	$⊢ ((A \in V \land X \in A) \land g \in B) \to S ((x \in A ⟼ g)) = (x \in A ⟼ g) (X)$
25		eqidd	$⊢ (A \in V \land X \in A) \to (x \in A ⟼ g) = (x \in A ⟼ g)$
26		eqidd	$⊢ ((A \in V \land X \in A) \land x = X) \to g = g$
27		simpr	$⊢ (A \in V \land X \in A) \to X \in A$
28		vex	$⊢ g \in V$
29	28	a1i	$⊢ (A \in V \land X \in A) \to g \in V$
30	25 26 27 29	fvmptd	$⊢ (A \in V \land X \in A) \to (x \in A ⟼ g) (X) = g$
31	30	adantr	$⊢ ((A \in V \land X \in A) \land g \in B) \to (x \in A ⟼ g) (X) = g$
32	24 31	eqtr2d	$⊢ ((A \in V \land X \in A) \land g \in B) \to g = S ((x \in A ⟼ g))$
33	13 16 32	rspcedvd	$⊢ ((A \in V \land X \in A) \land g \in B) \to \exists h \in F g = S (h)$
34	33	ralrimiva	$⊢ (A \in V \land X \in A) \to \forall g \in B \exists h \in F g = S (h)$
35		dffo3	$⊢ S : F \underset{onto}{⟶} B \leftrightarrow (S : F ⟶ B \land \forall g \in B \exists h \in F g = S (h))$
36	4 34 35	sylanbrc	$⊢ (A \in V \land X \in A) \to S : F \underset{onto}{⟶} B$

Metamath Proof Explorer

Theorem fsetfocdm

Proof