Metamath Proof Explorer


Theorem 1stpreima

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

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

Proof

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