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 
|- ( A C_ B -> ( `' ( 1st |` ( B X. C ) ) " A ) = ( A X. C ) )

Proof

Step Hyp Ref Expression
1 elxp7 
 |-  ( w e. ( B X. C ) <-> ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) )
2 1 anbi2i 
 |-  ( ( ( 1st ` w ) e. A /\ w e. ( B X. C ) ) <-> ( ( 1st ` w ) e. A /\ ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) ) )
3 anass 
 |-  ( ( ( ( 1st ` w ) e. A /\ ( 1st ` w ) e. B ) /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) <-> ( ( 1st ` w ) e. A /\ ( ( 1st ` w ) e. B /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) ) )
4 3 a1i 
 |-  ( A C_ B -> ( ( ( ( 1st ` w ) e. A /\ ( 1st ` w ) e. B ) /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) <-> ( ( 1st ` w ) e. A /\ ( ( 1st ` w ) e. B /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) ) ) )
5 ssel 
 |-  ( A C_ B -> ( ( 1st ` w ) e. A -> ( 1st ` w ) e. B ) )
6 5 pm4.71d 
 |-  ( A C_ B -> ( ( 1st ` w ) e. A <-> ( ( 1st ` w ) e. A /\ ( 1st ` w ) e. B ) ) )
7 6 anbi1d 
 |-  ( A C_ B -> ( ( ( 1st ` w ) e. A /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) <-> ( ( ( 1st ` w ) e. A /\ ( 1st ` w ) e. B ) /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) ) )
8 an12 
 |-  ( ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) <-> ( ( 1st ` w ) e. B /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) )
9 8 anbi2i 
 |-  ( ( ( 1st ` w ) e. A /\ ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) ) <-> ( ( 1st ` w ) e. A /\ ( ( 1st ` w ) e. B /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) ) )
10 9 a1i 
 |-  ( A C_ B -> ( ( ( 1st ` w ) e. A /\ ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) ) <-> ( ( 1st ` w ) e. A /\ ( ( 1st ` w ) e. B /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) ) ) )
11 4 7 10 3bitr4d 
 |-  ( A C_ B -> ( ( ( 1st ` w ) e. A /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) <-> ( ( 1st ` w ) e. A /\ ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) ) ) )
12 2 11 bitr4id 
 |-  ( A C_ B -> ( ( ( 1st ` w ) e. A /\ w e. ( B X. C ) ) <-> ( ( 1st ` w ) e. A /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) ) )
13 an12 
 |-  ( ( ( 1st ` w ) e. A /\ ( w e. ( _V X. _V ) /\ ( 2nd ` w ) e. C ) ) <-> ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. A /\ ( 2nd ` w ) e. C ) ) )
14 12 13 bitrdi 
 |-  ( A C_ B -> ( ( ( 1st ` w ) e. A /\ w e. ( B X. C ) ) <-> ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. A /\ ( 2nd ` w ) e. C ) ) ) )
15 cnvresima 
 |-  ( `' ( 1st |` ( B X. C ) ) " A ) = ( ( `' 1st " A ) i^i ( B X. C ) )
16 15 eleq2i 
 |-  ( w e. ( `' ( 1st |` ( B X. C ) ) " A ) <-> w e. ( ( `' 1st " A ) i^i ( B X. C ) ) )
17 elin 
 |-  ( w e. ( ( `' 1st " A ) i^i ( B X. C ) ) <-> ( w e. ( `' 1st " A ) /\ w e. ( B X. C ) ) )
18 vex 
 |-  w e. _V
19 fo1st 
 |-  1st : _V -onto-> _V
20 fofn 
 |-  ( 1st : _V -onto-> _V -> 1st Fn _V )
21 elpreima 
 |-  ( 1st Fn _V -> ( w e. ( `' 1st " A ) <-> ( w e. _V /\ ( 1st ` w ) e. A ) ) )
22 19 20 21 mp2b 
 |-  ( w e. ( `' 1st " A ) <-> ( w e. _V /\ ( 1st ` w ) e. A ) )
23 18 22 mpbiran 
 |-  ( w e. ( `' 1st " A ) <-> ( 1st ` w ) e. A )
24 23 anbi1i 
 |-  ( ( w e. ( `' 1st " A ) /\ w e. ( B X. C ) ) <-> ( ( 1st ` w ) e. A /\ w e. ( B X. C ) ) )
25 16 17 24 3bitri 
 |-  ( w e. ( `' ( 1st |` ( B X. C ) ) " A ) <-> ( ( 1st ` w ) e. A /\ w e. ( B X. C ) ) )
26 elxp7 
 |-  ( w e. ( A X. C ) <-> ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. A /\ ( 2nd ` w ) e. C ) ) )
27 14 25 26 3bitr4g 
 |-  ( A C_ B -> ( w e. ( `' ( 1st |` ( B X. C ) ) " A ) <-> w e. ( A X. C ) ) )
28 27 eqrdv 
 |-  ( A C_ B -> ( `' ( 1st |` ( B X. C ) ) " A ) = ( A X. C ) )