Metamath Proof Explorer

Theorem 2ndpreima

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

Ref Expression
Assertion 2ndpreima 
|- ( A C_ C -> ( `' ( 2nd |` ( B X. C ) ) " A ) = ( B X. A ) )

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 anbi1i 
 |-  ( ( w e. ( B X. C ) /\ ( 2nd ` w ) e. A ) <-> ( ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) /\ ( 2nd ` w ) e. A ) )
3 ssel 
 |-  ( A C_ C -> ( ( 2nd ` w ) e. A -> ( 2nd ` w ) e. C ) )
4 3 pm4.71rd 
 |-  ( A C_ C -> ( ( 2nd ` w ) e. A <-> ( ( 2nd ` w ) e. C /\ ( 2nd ` w ) e. A ) ) )
5 4 anbi2d 
 |-  ( A C_ C -> ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( 2nd ` w ) e. A ) <-> ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( ( 2nd ` w ) e. C /\ ( 2nd ` w ) e. A ) ) ) )
6 anass 
 |-  ( ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( 2nd ` w ) e. C ) /\ ( 2nd ` w ) e. A ) <-> ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( ( 2nd ` w ) e. C /\ ( 2nd ` w ) e. A ) ) )
7 6 bicomi 
 |-  ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( ( 2nd ` w ) e. C /\ ( 2nd ` w ) e. A ) ) <-> ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( 2nd ` w ) e. C ) /\ ( 2nd ` w ) e. A ) )
8 7 a1i 
 |-  ( A C_ C -> ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( ( 2nd ` w ) e. C /\ ( 2nd ` w ) e. A ) ) <-> ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( 2nd ` w ) e. C ) /\ ( 2nd ` w ) e. A ) ) )
9 anass 
 |-  ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( 2nd ` w ) e. C ) <-> ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) )
10 9 anbi1i 
 |-  ( ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( 2nd ` w ) e. C ) /\ ( 2nd ` w ) e. A ) <-> ( ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) /\ ( 2nd ` w ) e. A ) )
11 10 a1i 
 |-  ( A C_ C -> ( ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( 2nd ` w ) e. C ) /\ ( 2nd ` w ) e. A ) <-> ( ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) /\ ( 2nd ` w ) e. A ) ) )
12 5 8 11 3bitrd 
 |-  ( A C_ C -> ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( 2nd ` w ) e. A ) <-> ( ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. C ) ) /\ ( 2nd ` w ) e. A ) ) )
13 2 12 bitr4id 
 |-  ( A C_ C -> ( ( w e. ( B X. C ) /\ ( 2nd ` w ) e. A ) <-> ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( 2nd ` w ) e. A ) ) )
14 ancom 
 |-  ( ( w e. ( B X. C ) /\ ( 2nd ` w ) e. A ) <-> ( ( 2nd ` w ) e. A /\ w e. ( B X. C ) ) )
15 anass 
 |-  ( ( ( w e. ( _V X. _V ) /\ ( 1st ` w ) e. B ) /\ ( 2nd ` w ) e. A ) <-> ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. A ) ) )
16 13 14 15 3bitr3g 
 |-  ( A C_ C -> ( ( ( 2nd ` w ) e. A /\ w e. ( B X. C ) ) <-> ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. A ) ) ) )
17 cnvresima 
 |-  ( `' ( 2nd |` ( B X. C ) ) " A ) = ( ( `' 2nd " A ) i^i ( B X. C ) )
18 17 eleq2i 
 |-  ( w e. ( `' ( 2nd |` ( B X. C ) ) " A ) <-> w e. ( ( `' 2nd " A ) i^i ( B X. C ) ) )
19 elin 
 |-  ( w e. ( ( `' 2nd " A ) i^i ( B X. C ) ) <-> ( w e. ( `' 2nd " A ) /\ w e. ( B X. C ) ) )
20 vex 
 |-  w e. _V
21 fo2nd 
 |-  2nd : _V -onto-> _V
22 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
23 elpreima 
 |-  ( 2nd Fn _V -> ( w e. ( `' 2nd " A ) <-> ( w e. _V /\ ( 2nd ` w ) e. A ) ) )
24 21 22 23 mp2b 
 |-  ( w e. ( `' 2nd " A ) <-> ( w e. _V /\ ( 2nd ` w ) e. A ) )
25 20 24 mpbiran 
 |-  ( w e. ( `' 2nd " A ) <-> ( 2nd ` w ) e. A )
26 25 anbi1i 
 |-  ( ( w e. ( `' 2nd " A ) /\ w e. ( B X. C ) ) <-> ( ( 2nd ` w ) e. A /\ w e. ( B X. C ) ) )
27 18 19 26 3bitri 
 |-  ( w e. ( `' ( 2nd |` ( B X. C ) ) " A ) <-> ( ( 2nd ` w ) e. A /\ w e. ( B X. C ) ) )
28 elxp7 
 |-  ( w e. ( B X. A ) <-> ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. B /\ ( 2nd ` w ) e. A ) ) )
29 16 27 28 3bitr4g 
 |-  ( A C_ C -> ( w e. ( `' ( 2nd |` ( B X. C ) ) " A ) <-> w e. ( B X. A ) ) )
30 29 eqrdv 
 |-  ( A C_ C -> ( `' ( 2nd |` ( B X. C ) ) " A ) = ( B X. A ) )