Metamath Proof Explorer

Theorem ptpjpre1

Description: The preimage of a projection function can be expressed as an indexed cartesian product. (Contributed by Mario Carneiro, 6-Feb-2015)

Ref Expression
Hypothesis ptpjpre1.1 
|- X = X_ k e. A U. ( F ` k )
Assertion ptpjpre1 
|- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( `' ( w e. X |-> ( w ` I ) ) " U ) = X_ k e. A if ( k = I , U , U. ( F ` k ) ) )

Proof

Step Hyp Ref Expression
1 ptpjpre1.1 
 |-  X = X_ k e. A U. ( F ` k )
2 fveq2 
 |-  ( k = I -> ( w ` k ) = ( w ` I ) )
3 fveq2 
 |-  ( k = I -> ( F ` k ) = ( F ` I ) )
4 3 unieqd 
 |-  ( k = I -> U. ( F ` k ) = U. ( F ` I ) )
5 2 4 eleq12d 
 |-  ( k = I -> ( ( w ` k ) e. U. ( F ` k ) <-> ( w ` I ) e. U. ( F ` I ) ) )
6 vex 
 |-  w e. _V
7 6 elixp 
 |-  ( w e. X_ k e. A U. ( F ` k ) <-> ( w Fn A /\ A. k e. A ( w ` k ) e. U. ( F ` k ) ) )
8 7 simprbi 
 |-  ( w e. X_ k e. A U. ( F ` k ) -> A. k e. A ( w ` k ) e. U. ( F ` k ) )
9 8 1 eleq2s 
 |-  ( w e. X -> A. k e. A ( w ` k ) e. U. ( F ` k ) )
10 9 adantl 
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ w e. X ) -> A. k e. A ( w ` k ) e. U. ( F ` k ) )
11 simplrl 
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ w e. X ) -> I e. A )
12 5 10 11 rspcdva 
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ w e. X ) -> ( w ` I ) e. U. ( F ` I ) )
13 12 fmpttd 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( w e. X |-> ( w ` I ) ) : X --> U. ( F ` I ) )
14 ffn 
 |-  ( ( w e. X |-> ( w ` I ) ) : X --> U. ( F ` I ) -> ( w e. X |-> ( w ` I ) ) Fn X )
15 elpreima 
 |-  ( ( w e. X |-> ( w ` I ) ) Fn X -> ( z e. ( `' ( w e. X |-> ( w ` I ) ) " U ) <-> ( z e. X /\ ( ( w e. X |-> ( w ` I ) ) ` z ) e. U ) ) )
16 13 14 15 3syl 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( z e. ( `' ( w e. X |-> ( w ` I ) ) " U ) <-> ( z e. X /\ ( ( w e. X |-> ( w ` I ) ) ` z ) e. U ) ) )
17 fveq1 
 |-  ( w = z -> ( w ` I ) = ( z ` I ) )
18 eqid 
 |-  ( w e. X |-> ( w ` I ) ) = ( w e. X |-> ( w ` I ) )
19 fvex 
 |-  ( z ` I ) e. _V
20 17 18 19 fvmpt 
 |-  ( z e. X -> ( ( w e. X |-> ( w ` I ) ) ` z ) = ( z ` I ) )
21 20 eleq1d 
 |-  ( z e. X -> ( ( ( w e. X |-> ( w ` I ) ) ` z ) e. U <-> ( z ` I ) e. U ) )
22 21 pm5.32i 
 |-  ( ( z e. X /\ ( ( w e. X |-> ( w ` I ) ) ` z ) e. U ) <-> ( z e. X /\ ( z ` I ) e. U ) )
23 1 eleq2i 
 |-  ( z e. X <-> z e. X_ k e. A U. ( F ` k ) )
24 vex 
 |-  z e. _V
25 24 elixp 
 |-  ( z e. X_ k e. A U. ( F ` k ) <-> ( z Fn A /\ A. k e. A ( z ` k ) e. U. ( F ` k ) ) )
26 23 25 bitri 
 |-  ( z e. X <-> ( z Fn A /\ A. k e. A ( z ` k ) e. U. ( F ` k ) ) )
27 26 anbi1i 
 |-  ( ( z e. X /\ ( z ` I ) e. U ) <-> ( ( z Fn A /\ A. k e. A ( z ` k ) e. U. ( F ` k ) ) /\ ( z ` I ) e. U ) )
28 anass 
 |-  ( ( ( z Fn A /\ A. k e. A ( z ` k ) e. U. ( F ` k ) ) /\ ( z ` I ) e. U ) <-> ( z Fn A /\ ( A. k e. A ( z ` k ) e. U. ( F ` k ) /\ ( z ` I ) e. U ) ) )
29 27 28 bitri 
 |-  ( ( z e. X /\ ( z ` I ) e. U ) <-> ( z Fn A /\ ( A. k e. A ( z ` k ) e. U. ( F ` k ) /\ ( z ` I ) e. U ) ) )
30 22 29 bitri 
 |-  ( ( z e. X /\ ( ( w e. X |-> ( w ` I ) ) ` z ) e. U ) <-> ( z Fn A /\ ( A. k e. A ( z ` k ) e. U. ( F ` k ) /\ ( z ` I ) e. U ) ) )
31 simprl 
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ ( ( z ` I ) e. U /\ ( z ` k ) e. U. ( F ` k ) ) ) -> ( z ` I ) e. U )
32 fveq2 
 |-  ( k = I -> ( z ` k ) = ( z ` I ) )
33 iftrue 
 |-  ( k = I -> if ( k = I , U , U. ( F ` k ) ) = U )
34 32 33 eleq12d 
 |-  ( k = I -> ( ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) <-> ( z ` I ) e. U ) )
35 31 34 syl5ibrcom 
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ ( ( z ` I ) e. U /\ ( z ` k ) e. U. ( F ` k ) ) ) -> ( k = I -> ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) )
36 simprr 
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ ( ( z ` I ) e. U /\ ( z ` k ) e. U. ( F ` k ) ) ) -> ( z ` k ) e. U. ( F ` k ) )
37 iffalse 
 |-  ( -. k = I -> if ( k = I , U , U. ( F ` k ) ) = U. ( F ` k ) )
38 37 eleq2d 
 |-  ( -. k = I -> ( ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) <-> ( z ` k ) e. U. ( F ` k ) ) )
39 36 38 syl5ibrcom 
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ ( ( z ` I ) e. U /\ ( z ` k ) e. U. ( F ` k ) ) ) -> ( -. k = I -> ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) )
40 35 39 pm2.61d 
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ ( ( z ` I ) e. U /\ ( z ` k ) e. U. ( F ` k ) ) ) -> ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) )
41 40 expr 
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ ( z ` I ) e. U ) -> ( ( z ` k ) e. U. ( F ` k ) -> ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) )
42 41 ralimdv 
 |-  ( ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) /\ ( z ` I ) e. U ) -> ( A. k e. A ( z ` k ) e. U. ( F ` k ) -> A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) )
43 42 expimpd 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( ( ( z ` I ) e. U /\ A. k e. A ( z ` k ) e. U. ( F ` k ) ) -> A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) )
44 43 ancomsd 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( ( A. k e. A ( z ` k ) e. U. ( F ` k ) /\ ( z ` I ) e. U ) -> A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) )
45 elssuni 
 |-  ( U e. ( F ` I ) -> U C_ U. ( F ` I ) )
46 45 ad2antll 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> U C_ U. ( F ` I ) )
47 33 4 sseq12d 
 |-  ( k = I -> ( if ( k = I , U , U. ( F ` k ) ) C_ U. ( F ` k ) <-> U C_ U. ( F ` I ) ) )
48 46 47 syl5ibrcom 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( k = I -> if ( k = I , U , U. ( F ` k ) ) C_ U. ( F ` k ) ) )
49 ssid 
 |-  U. ( F ` k ) C_ U. ( F ` k )
50 37 49 eqsstrdi 
 |-  ( -. k = I -> if ( k = I , U , U. ( F ` k ) ) C_ U. ( F ` k ) )
51 48 50 pm2.61d1 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> if ( k = I , U , U. ( F ` k ) ) C_ U. ( F ` k ) )
52 51 sseld 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) -> ( z ` k ) e. U. ( F ` k ) ) )
53 52 ralimdv 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) -> A. k e. A ( z ` k ) e. U. ( F ` k ) ) )
54 34 rspcv 
 |-  ( I e. A -> ( A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) -> ( z ` I ) e. U ) )
55 54 ad2antrl 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) -> ( z ` I ) e. U ) )
56 53 55 jcad 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) -> ( A. k e. A ( z ` k ) e. U. ( F ` k ) /\ ( z ` I ) e. U ) ) )
57 44 56 impbid 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( ( A. k e. A ( z ` k ) e. U. ( F ` k ) /\ ( z ` I ) e. U ) <-> A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) )
58 57 anbi2d 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( ( z Fn A /\ ( A. k e. A ( z ` k ) e. U. ( F ` k ) /\ ( z ` I ) e. U ) ) <-> ( z Fn A /\ A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) ) )
59 30 58 syl5bb 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( ( z e. X /\ ( ( w e. X |-> ( w ` I ) ) ` z ) e. U ) <-> ( z Fn A /\ A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) ) )
60 16 59 bitrd 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( z e. ( `' ( w e. X |-> ( w ` I ) ) " U ) <-> ( z Fn A /\ A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) ) )
61 24 elixp 
 |-  ( z e. X_ k e. A if ( k = I , U , U. ( F ` k ) ) <-> ( z Fn A /\ A. k e. A ( z ` k ) e. if ( k = I , U , U. ( F ` k ) ) ) )
62 60 61 bitr4di 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( z e. ( `' ( w e. X |-> ( w ` I ) ) " U ) <-> z e. X_ k e. A if ( k = I , U , U. ( F ` k ) ) ) )
63 62 eqrdv 
 |-  ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ U e. ( F ` I ) ) ) -> ( `' ( w e. X |-> ( w ` I ) ) " U ) = X_ k e. A if ( k = I , U , U. ( F ` k ) ) )