xp1st

Description: Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	xp1st	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ( 1^st ‘ 𝐴 ) ∈ 𝐵 )

Step	Hyp	Ref	Expression
1		elxp	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑏 ∃ 𝑐 ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) )
2		vex	⊢ 𝑏 ∈ V
3		vex	⊢ 𝑐 ∈ V
4	2 3	op1std	⊢ ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ → ( 1^st ‘ 𝐴 ) = 𝑏 )
5	4	eleq1d	⊢ ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ → ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵 ) )
6	5	biimpar	⊢ ( ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑏 ∈ 𝐵 ) → ( 1^st ‘ 𝐴 ) ∈ 𝐵 )
7	6	adantrr	⊢ ( ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 1^st ‘ 𝐴 ) ∈ 𝐵 )
8	7	exlimivv	⊢ ( ∃ 𝑏 ∃ 𝑐 ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 1^st ‘ 𝐴 ) ∈ 𝐵 )
9	1 8	sylbi	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ( 1^st ‘ 𝐴 ) ∈ 𝐵 )

Metamath Proof Explorer