Theorem 2ndpreima

Description: The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017)

	Ref	Expression
Assertion	2ndpreima	⊢ ( 𝐴 ⊆ 𝐶 → ( ◡ ( 2nd ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) = ( 𝐵 × 𝐴 ) )

Proof

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