1stpreima

Description: The preimage by 1st is a 'vertical band'. (Contributed by Thierry Arnoux, 13-Oct-2017)

		Ref	Expression
	Assertion	1stpreima	⊢ ( 𝐴 ⊆ 𝐵 → ( ^◡ ( 1^st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) = ( 𝐴 × 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elxp7	⊢ ( 𝑤 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) )
2	1	anbi2i	⊢ ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) )
3		anass	⊢ ( ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 1^st ‘ 𝑤 ) ∈ 𝐵 ) ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) )
4	3	a1i	⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 1^st ‘ 𝑤 ) ∈ 𝐵 ) ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) )
5		ssel	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 → ( 1^st ‘ 𝑤 ) ∈ 𝐵 ) )
6	5	pm4.71d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 1^st ‘ 𝑤 ) ∈ 𝐵 ) ) )
7	6	anbi1d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 1^st ‘ 𝑤 ) ∈ 𝐵 ) ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) )
8		an12	⊢ ( ( 𝑤 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) )
9	8	anbi2i	⊢ ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) )
10	9	a1i	⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) )
11	4 7 10	3bitr4d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) )
12	2 11	bitr4id	⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) )
13		an12	⊢ ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) )
14	12 13	bitrdi	⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) )
15		cnvresima	⊢ ( ^◡ ( 1^st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) = ( ( ^◡ 1^st “ 𝐴 ) ∩ ( 𝐵 × 𝐶 ) )
16	15	eleq2i	⊢ ( 𝑤 ∈ ( ^◡ ( 1^st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) ↔ 𝑤 ∈ ( ( ^◡ 1^st “ 𝐴 ) ∩ ( 𝐵 × 𝐶 ) ) )
17		elin	⊢ ( 𝑤 ∈ ( ( ^◡ 1^st “ 𝐴 ) ∩ ( 𝐵 × 𝐶 ) ) ↔ ( 𝑤 ∈ ( ^◡ 1^st “ 𝐴 ) ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) )
18		vex	⊢ 𝑤 ∈ V
19		fo1st	⊢ 1^st : V –onto→ V
20		fofn	⊢ ( 1^st : V –onto→ V → 1^st Fn V )
21		elpreima	⊢ ( 1^st Fn V → ( 𝑤 ∈ ( ^◡ 1^st “ 𝐴 ) ↔ ( 𝑤 ∈ V ∧ ( 1^st ‘ 𝑤 ) ∈ 𝐴 ) ) )
22	19 20 21	mp2b	⊢ ( 𝑤 ∈ ( ^◡ 1^st “ 𝐴 ) ↔ ( 𝑤 ∈ V ∧ ( 1^st ‘ 𝑤 ) ∈ 𝐴 ) )
23	18 22	mpbiran	⊢ ( 𝑤 ∈ ( ^◡ 1^st “ 𝐴 ) ↔ ( 1^st ‘ 𝑤 ) ∈ 𝐴 )
24	23	anbi1i	⊢ ( ( 𝑤 ∈ ( ^◡ 1^st “ 𝐴 ) ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) )
25	16 17 24	3bitri	⊢ ( 𝑤 ∈ ( ^◡ ( 1^st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) ↔ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) )
26		elxp7	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐶 ) ↔ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 2^nd ‘ 𝑤 ) ∈ 𝐶 ) ) )
27	14 25 26	3bitr4g	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑤 ∈ ( ^◡ ( 1^st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) ↔ 𝑤 ∈ ( 𝐴 × 𝐶 ) ) )
28	27	eqrdv	⊢ ( 𝐴 ⊆ 𝐵 → ( ^◡ ( 1^st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) = ( 𝐴 × 𝐶 ) )

Metamath Proof Explorer

Theorem 1stpreima

Proof