unielxp

Description: The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006)

		Ref	Expression
	Assertion	unielxp	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ∪ 𝐴 ∈ ∪ ( 𝐵 × 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elxp7	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) )
2		elvvuni	⊢ ( 𝐴 ∈ ( V × V ) → ∪ 𝐴 ∈ 𝐴 )
3	2	adantr	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) → ∪ 𝐴 ∈ 𝐴 )
4		simprl	⊢ ( ( ∪ 𝐴 ∈ 𝐴 ∧ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) ) → 𝐴 ∈ ( V × V ) )
5		eleq2	⊢ ( 𝑥 = 𝐴 → ( ∪ 𝐴 ∈ 𝑥 ↔ ∪ 𝐴 ∈ 𝐴 ) )
6		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( V × V ) ↔ 𝐴 ∈ ( V × V ) ) )
7		fveq2	⊢ ( 𝑥 = 𝐴 → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝐴 ) )
8	7	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ↔ ( 1^st ‘ 𝐴 ) ∈ 𝐵 ) )
9		fveq2	⊢ ( 𝑥 = 𝐴 → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝐴 ) )
10	9	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ↔ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) )
11	8 10	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) )
12	6 11	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) ) )
13	5 12	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ∪ 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ) ) ↔ ( ∪ 𝐴 ∈ 𝐴 ∧ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) ) ) )
14	13	spcegv	⊢ ( 𝐴 ∈ ( V × V ) → ( ( ∪ 𝐴 ∈ 𝐴 ∧ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) ) → ∃ 𝑥 ( ∪ 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ) ) ) )
15	4 14	mpcom	⊢ ( ( ∪ 𝐴 ∈ 𝐴 ∧ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) ) → ∃ 𝑥 ( ∪ 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ) ) )
16		eluniab	⊢ ( ∪ 𝐴 ∈ ∪ { 𝑥 ∣ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ) } ↔ ∃ 𝑥 ( ∪ 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ) ) )
17	15 16	sylibr	⊢ ( ( ∪ 𝐴 ∈ 𝐴 ∧ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) ) → ∪ 𝐴 ∈ ∪ { 𝑥 ∣ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ) } )
18		xp2	⊢ ( 𝐵 × 𝐶 ) = { 𝑥 ∈ ( V × V ) ∣ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) }
19		df-rab	⊢ { 𝑥 ∈ ( V × V ) ∣ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) } = { 𝑥 ∣ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ) }
20	18 19	eqtri	⊢ ( 𝐵 × 𝐶 ) = { 𝑥 ∣ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ) }
21	20	unieqi	⊢ ∪ ( 𝐵 × 𝐶 ) = ∪ { 𝑥 ∣ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝐶 ) ) }
22	17 21	eleqtrrdi	⊢ ( ( ∪ 𝐴 ∈ 𝐴 ∧ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) ) → ∪ 𝐴 ∈ ∪ ( 𝐵 × 𝐶 ) )
23	3 22	mpancom	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝐶 ) ) → ∪ 𝐴 ∈ ∪ ( 𝐵 × 𝐶 ) )
24	1 23	sylbi	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ∪ 𝐴 ∈ ∪ ( 𝐵 × 𝐶 ) )

Metamath Proof Explorer

Theorem unielxp

Proof