Metamath Proof Explorer

Theorem elxp8

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp7 . (Contributed by ML, 19-Oct-2020)

		Ref	Expression
	Assertion	elxp8	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐴 ∈ ( V × 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xp1st	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ( 1^st ‘ 𝐴 ) ∈ 𝐵 )
2		ssv	⊢ 𝐵 ⊆ V
3		ssid	⊢ 𝐶 ⊆ 𝐶
4		xpss12	⊢ ( ( 𝐵 ⊆ V ∧ 𝐶 ⊆ 𝐶 ) → ( 𝐵 × 𝐶 ) ⊆ ( V × 𝐶 ) )
5	2 3 4	mp2an	⊢ ( 𝐵 × 𝐶 ) ⊆ ( V × 𝐶 )
6	5	sseli	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → 𝐴 ∈ ( V × 𝐶 ) )
7	1 6	jca	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐴 ∈ ( V × 𝐶 ) ) )
8		xpss	⊢ ( V × 𝐶 ) ⊆ ( V × V )
9	8	sseli	⊢ ( 𝐴 ∈ ( V × 𝐶 ) → 𝐴 ∈ ( V × V ) )
10	9	adantl	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐴 ∈ ( V × 𝐶 ) ) → 𝐴 ∈ ( V × V ) )
11		xp2nd	⊢ ( 𝐴 ∈ ( V × 𝐶 ) → ( 2^nd ‘ 𝐴 ) ∈ 𝐶 )
12	11	anim2i	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐴 ∈ ( V × 𝐶 ) ) → ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) )
13		elxp7	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) )
14	10 12 13	sylanbrc	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐴 ∈ ( V × 𝐶 ) ) → 𝐴 ∈ ( 𝐵 × 𝐶 ) )
15	7 14	impbii	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐴 ∈ ( V × 𝐶 ) ) )