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	⊢ ( 𝐵 ≠ ∅ → ( 1^st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) –onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 )
2		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
3		fvres	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ( ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 1^st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
4		vex	⊢ 𝑥 ∈ V
5		vex	⊢ 𝑦 ∈ V
6	4 5	op1st	⊢ ( 1^st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑥
7	3 6	eqtr2di	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → 𝑥 = ( ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
8		f1stres	⊢ ( 1^st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐴
9		ffn	⊢ ( ( 1^st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐴 → ( 1^st ↾ ( 𝐴 × 𝐵 ) ) Fn ( 𝐴 × 𝐵 ) )
10	8 9	ax-mp	⊢ ( 1^st ↾ ( 𝐴 × 𝐵 ) ) Fn ( 𝐴 × 𝐵 )
11		fnfvelrn	⊢ ( ( ( 1^st ↾ ( 𝐴 × 𝐵 ) ) Fn ( 𝐴 × 𝐵 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ( ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) )
12	10 11	mpan	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ( ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) )
13	7 12	eqeltrd	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → 𝑥 ∈ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) )
14	2 13	sylbir	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) )
15	14	expcom	⊢ ( 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ) )
16	15	exlimiv	⊢ ( ∃ 𝑦 𝑦 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ) )
17	1 16	sylbi	⊢ ( 𝐵 ≠ ∅ → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ) )
18	17	ssrdv	⊢ ( 𝐵 ≠ ∅ → 𝐴 ⊆ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) )
19		frn	⊢ ( ( 1^st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐴 → ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ⊆ 𝐴 )
20	8 19	ax-mp	⊢ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ⊆ 𝐴
21	18 20	jctil	⊢ ( 𝐵 ≠ ∅ → ( ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ) )
22		eqss	⊢ ( ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) = 𝐴 ↔ ( ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) ) )
23	21 22	sylibr	⊢ ( 𝐵 ≠ ∅ → ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) = 𝐴 )
24	23 8	jctil	⊢ ( 𝐵 ≠ ∅ → ( ( 1^st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐴 ∧ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) = 𝐴 ) )
25		dffo2	⊢ ( ( 1^st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) –onto→ 𝐴 ↔ ( ( 1^st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) ⟶ 𝐴 ∧ ran ( 1^st ↾ ( 𝐴 × 𝐵 ) ) = 𝐴 ) )
26	24 25	sylibr	⊢ ( 𝐵 ≠ ∅ → ( 1^st ↾ ( 𝐴 × 𝐵 ) ) : ( 𝐴 × 𝐵 ) –onto→ 𝐴 )

Metamath Proof Explorer

Theorem fo1stres

Proof