fo1stres

Description: Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 14-Dec-2008)

		Ref	Expression
	Assertion	fo1stres	$⊢ B \neq \emptyset \to ({1^{st} ↾}_{(A \times B)}) : A \times B \underset{onto}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ B \neq \emptyset \leftrightarrow \exists y y \in B$
2		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
3		fvres	$⊢ ⟨x, y⟩ \in (A \times B) \to ({1^{st} ↾}_{(A \times B)}) (⟨x, y⟩) = 1^{st} (⟨x, y⟩)$
4		vex	$⊢ x \in V$
5		vex	$⊢ y \in V$
6	4 5	op1st	$⊢ 1^{st} (⟨x, y⟩) = x$
7	3 6	eqtr2di	$⊢ ⟨x, y⟩ \in (A \times B) \to x = ({1^{st} ↾}_{(A \times B)}) (⟨x, y⟩)$
8		f1stres	$⊢ ({1^{st} ↾}_{(A \times B)}) : A \times B ⟶ A$
9		ffn	$⊢ ({1^{st} ↾}_{(A \times B)}) : A \times B ⟶ A \to ({1^{st} ↾}_{(A \times B)}) Fn (A \times B)$
10	8 9	ax-mp	$⊢ ({1^{st} ↾}_{(A \times B)}) Fn (A \times B)$
11		fnfvelrn	$⊢ (({1^{st} ↾}_{(A \times B)}) Fn (A \times B) \land ⟨x, y⟩ \in (A \times B)) \to ({1^{st} ↾}_{(A \times B)}) (⟨x, y⟩) \in ran ({1^{st} ↾}_{(A \times B)})$
12	10 11	mpan	$⊢ ⟨x, y⟩ \in (A \times B) \to ({1^{st} ↾}_{(A \times B)}) (⟨x, y⟩) \in ran ({1^{st} ↾}_{(A \times B)})$
13	7 12	eqeltrd	$⊢ ⟨x, y⟩ \in (A \times B) \to x \in ran ({1^{st} ↾}_{(A \times B)})$
14	2 13	sylbir	$⊢ (x \in A \land y \in B) \to x \in ran ({1^{st} ↾}_{(A \times B)})$
15	14	expcom	$⊢ y \in B \to (x \in A \to x \in ran ({1^{st} ↾}_{(A \times B)}))$
16	15	exlimiv	$⊢ \exists y y \in B \to (x \in A \to x \in ran ({1^{st} ↾}_{(A \times B)}))$
17	1 16	sylbi	$⊢ B \neq \emptyset \to (x \in A \to x \in ran ({1^{st} ↾}_{(A \times B)}))$
18	17	ssrdv	$⊢ B \neq \emptyset \to A \subseteq ran ({1^{st} ↾}_{(A \times B)})$
19		frn	$⊢ ({1^{st} ↾}_{(A \times B)}) : A \times B ⟶ A \to ran ({1^{st} ↾}_{(A \times B)}) \subseteq A$
20	8 19	ax-mp	$⊢ ran ({1^{st} ↾}_{(A \times B)}) \subseteq A$
21	18 20	jctil	$⊢ B \neq \emptyset \to (ran ({1^{st} ↾}_{(A \times B)}) \subseteq A \land A \subseteq ran ({1^{st} ↾}_{(A \times B)}))$
22		eqss	$⊢ ran ({1^{st} ↾}_{(A \times B)}) = A \leftrightarrow (ran ({1^{st} ↾}_{(A \times B)}) \subseteq A \land A \subseteq ran ({1^{st} ↾}_{(A \times B)}))$
23	21 22	sylibr	$⊢ B \neq \emptyset \to ran ({1^{st} ↾}_{(A \times B)}) = A$
24	23 8	jctil	$⊢ B \neq \emptyset \to (({1^{st} ↾}_{(A \times B)}) : A \times B ⟶ A \land ran ({1^{st} ↾}_{(A \times B)}) = A)$
25		dffo2	$⊢ ({1^{st} ↾}_{(A \times B)}) : A \times B \underset{onto}{⟶} A \leftrightarrow (({1^{st} ↾}_{(A \times B)}) : A \times B ⟶ A \land ran ({1^{st} ↾}_{(A \times B)}) = A)$
26	24 25	sylibr	$⊢ B \neq \emptyset \to ({1^{st} ↾}_{(A \times B)}) : A \times B \underset{onto}{⟶} A$

Metamath Proof Explorer

Theorem fo1stres

Proof