Metamath Proof Explorer

Theorem pw2f1olem

Description: Lemma for pw2f1o . (Contributed by Mario Carneiro, 6-Oct-2014)

Ref Expression
Hypotheses pw2f1o.1 
|- ( ph -> A e. V )
pw2f1o.2 
|- ( ph -> B e. W )
pw2f1o.3 
|- ( ph -> C e. W )
pw2f1o.4 
|- ( ph -> B =/= C )
Assertion pw2f1olem 
|- ( ph -> ( ( S e. ~P A /\ G = ( z e. A |-> if ( z e. S , C , B ) ) ) <-> ( G e. ( { B , C } ^m A ) /\ S = ( `' G " { C } ) ) ) )

Proof

Step Hyp Ref Expression
1 pw2f1o.1 
 |-  ( ph -> A e. V )
2 pw2f1o.2 
 |-  ( ph -> B e. W )
3 pw2f1o.3 
 |-  ( ph -> C e. W )
4 pw2f1o.4 
 |-  ( ph -> B =/= C )
5 prid2g 
 |-  ( C e. W -> C e. { B , C } )
6 3 5 syl 
 |-  ( ph -> C e. { B , C } )
7 prid1g 
 |-  ( B e. W -> B e. { B , C } )
8 2 7 syl 
 |-  ( ph -> B e. { B , C } )
9 6 8 ifcld 
 |-  ( ph -> if ( y e. S , C , B ) e. { B , C } )
10 9 adantr 
 |-  ( ( ph /\ y e. A ) -> if ( y e. S , C , B ) e. { B , C } )
11 10 fmpttd 
 |-  ( ph -> ( y e. A |-> if ( y e. S , C , B ) ) : A --> { B , C } )
12 11 adantr 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> ( y e. A |-> if ( y e. S , C , B ) ) : A --> { B , C } )
13 simprr 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> G = ( y e. A |-> if ( y e. S , C , B ) ) )
14 13 feq1d 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> ( G : A --> { B , C } <-> ( y e. A |-> if ( y e. S , C , B ) ) : A --> { B , C } ) )
15 12 14 mpbird 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> G : A --> { B , C } )
16 iftrue 
 |-  ( x e. S -> if ( x e. S , C , B ) = C )
17 4 ad2antrr 
 |-  ( ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) /\ x e. A ) -> B =/= C )
18 iffalse 
 |-  ( -. x e. S -> if ( x e. S , C , B ) = B )
19 18 neeq1d 
 |-  ( -. x e. S -> ( if ( x e. S , C , B ) =/= C <-> B =/= C ) )
20 17 19 syl5ibrcom 
 |-  ( ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) /\ x e. A ) -> ( -. x e. S -> if ( x e. S , C , B ) =/= C ) )
21 20 necon4bd 
 |-  ( ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) /\ x e. A ) -> ( if ( x e. S , C , B ) = C -> x e. S ) )
22 16 21 impbid2 
 |-  ( ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) /\ x e. A ) -> ( x e. S <-> if ( x e. S , C , B ) = C ) )
23 simplrr 
 |-  ( ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) /\ x e. A ) -> G = ( y e. A |-> if ( y e. S , C , B ) ) )
24 23 fveq1d 
 |-  ( ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) /\ x e. A ) -> ( G ` x ) = ( ( y e. A |-> if ( y e. S , C , B ) ) ` x ) )
25 id 
 |-  ( x e. A -> x e. A )
26 6 8 ifcld 
 |-  ( ph -> if ( x e. S , C , B ) e. { B , C } )
27 26 adantr 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> if ( x e. S , C , B ) e. { B , C } )
28 eleq1w 
 |-  ( y = x -> ( y e. S <-> x e. S ) )
29 28 ifbid 
 |-  ( y = x -> if ( y e. S , C , B ) = if ( x e. S , C , B ) )
30 eqid 
 |-  ( y e. A |-> if ( y e. S , C , B ) ) = ( y e. A |-> if ( y e. S , C , B ) )
31 29 30 fvmptg 
 |-  ( ( x e. A /\ if ( x e. S , C , B ) e. { B , C } ) -> ( ( y e. A |-> if ( y e. S , C , B ) ) ` x ) = if ( x e. S , C , B ) )
32 25 27 31 syl2anr 
 |-  ( ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) /\ x e. A ) -> ( ( y e. A |-> if ( y e. S , C , B ) ) ` x ) = if ( x e. S , C , B ) )
33 24 32 eqtrd 
 |-  ( ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) /\ x e. A ) -> ( G ` x ) = if ( x e. S , C , B ) )
34 33 eqeq1d 
 |-  ( ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) /\ x e. A ) -> ( ( G ` x ) = C <-> if ( x e. S , C , B ) = C ) )
35 22 34 bitr4d 
 |-  ( ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) /\ x e. A ) -> ( x e. S <-> ( G ` x ) = C ) )
36 35 pm5.32da 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> ( ( x e. A /\ x e. S ) <-> ( x e. A /\ ( G ` x ) = C ) ) )
37 simprl 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> S C_ A )
38 37 sseld 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> ( x e. S -> x e. A ) )
39 38 pm4.71rd 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> ( x e. S <-> ( x e. A /\ x e. S ) ) )
40 ffn 
 |-  ( G : A --> { B , C } -> G Fn A )
41 15 40 syl 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> G Fn A )
42 fniniseg 
 |-  ( G Fn A -> ( x e. ( `' G " { C } ) <-> ( x e. A /\ ( G ` x ) = C ) ) )
43 41 42 syl 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> ( x e. ( `' G " { C } ) <-> ( x e. A /\ ( G ` x ) = C ) ) )
44 36 39 43 3bitr4d 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> ( x e. S <-> x e. ( `' G " { C } ) ) )
45 44 eqrdv 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> S = ( `' G " { C } ) )
46 15 45 jca 
 |-  ( ( ph /\ ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) -> ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) )
47 simprr 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> S = ( `' G " { C } ) )
48 cnvimass 
 |-  ( `' G " { C } ) C_ dom G
49 fdm 
 |-  ( G : A --> { B , C } -> dom G = A )
50 49 ad2antrl 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> dom G = A )
51 48 50 sseqtrid 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> ( `' G " { C } ) C_ A )
52 47 51 eqsstrd 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> S C_ A )
53 40 ad2antrl 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> G Fn A )
54 dffn5 
 |-  ( G Fn A <-> G = ( y e. A |-> ( G ` y ) ) )
55 53 54 sylib 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> G = ( y e. A |-> ( G ` y ) ) )
56 simplrr 
 |-  ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) -> S = ( `' G " { C } ) )
57 56 eleq2d 
 |-  ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) -> ( y e. S <-> y e. ( `' G " { C } ) ) )
58 fniniseg 
 |-  ( G Fn A -> ( y e. ( `' G " { C } ) <-> ( y e. A /\ ( G ` y ) = C ) ) )
59 53 58 syl 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> ( y e. ( `' G " { C } ) <-> ( y e. A /\ ( G ` y ) = C ) ) )
60 59 baibd 
 |-  ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) -> ( y e. ( `' G " { C } ) <-> ( G ` y ) = C ) )
61 57 60 bitrd 
 |-  ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) -> ( y e. S <-> ( G ` y ) = C ) )
62 61 biimpa 
 |-  ( ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) /\ y e. S ) -> ( G ` y ) = C )
63 iftrue 
 |-  ( y e. S -> if ( y e. S , C , B ) = C )
64 63 adantl 
 |-  ( ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) /\ y e. S ) -> if ( y e. S , C , B ) = C )
65 62 64 eqtr4d 
 |-  ( ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) /\ y e. S ) -> ( G ` y ) = if ( y e. S , C , B ) )
66 simprl 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> G : A --> { B , C } )
67 66 ffvelcdmda 
 |-  ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) -> ( G ` y ) e. { B , C } )
68 fvex 
 |-  ( G ` y ) e. _V
69 68 elpr 
 |-  ( ( G ` y ) e. { B , C } <-> ( ( G ` y ) = B \/ ( G ` y ) = C ) )
70 67 69 sylib 
 |-  ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) -> ( ( G ` y ) = B \/ ( G ` y ) = C ) )
71 70 ord 
 |-  ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) -> ( -. ( G ` y ) = B -> ( G ` y ) = C ) )
72 71 61 sylibrd 
 |-  ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) -> ( -. ( G ` y ) = B -> y e. S ) )
73 72 con1d 
 |-  ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) -> ( -. y e. S -> ( G ` y ) = B ) )
74 73 imp 
 |-  ( ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) /\ -. y e. S ) -> ( G ` y ) = B )
75 iffalse 
 |-  ( -. y e. S -> if ( y e. S , C , B ) = B )
76 75 adantl 
 |-  ( ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) /\ -. y e. S ) -> if ( y e. S , C , B ) = B )
77 74 76 eqtr4d 
 |-  ( ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) /\ -. y e. S ) -> ( G ` y ) = if ( y e. S , C , B ) )
78 65 77 pm2.61dan 
 |-  ( ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) /\ y e. A ) -> ( G ` y ) = if ( y e. S , C , B ) )
79 78 mpteq2dva 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> ( y e. A |-> ( G ` y ) ) = ( y e. A |-> if ( y e. S , C , B ) ) )
80 55 79 eqtrd 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> G = ( y e. A |-> if ( y e. S , C , B ) ) )
81 52 80 jca 
 |-  ( ( ph /\ ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) -> ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) )
82 46 81 impbida 
 |-  ( ph -> ( ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) <-> ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) )
83 elpw2g 
 |-  ( A e. V -> ( S e. ~P A <-> S C_ A ) )
84 1 83 syl 
 |-  ( ph -> ( S e. ~P A <-> S C_ A ) )
85 eleq1w 
 |-  ( z = y -> ( z e. S <-> y e. S ) )
86 85 ifbid 
 |-  ( z = y -> if ( z e. S , C , B ) = if ( y e. S , C , B ) )
87 86 cbvmptv 
 |-  ( z e. A |-> if ( z e. S , C , B ) ) = ( y e. A |-> if ( y e. S , C , B ) )
88 87 a1i 
 |-  ( ph -> ( z e. A |-> if ( z e. S , C , B ) ) = ( y e. A |-> if ( y e. S , C , B ) ) )
89 88 eqeq2d 
 |-  ( ph -> ( G = ( z e. A |-> if ( z e. S , C , B ) ) <-> G = ( y e. A |-> if ( y e. S , C , B ) ) ) )
90 84 89 anbi12d 
 |-  ( ph -> ( ( S e. ~P A /\ G = ( z e. A |-> if ( z e. S , C , B ) ) ) <-> ( S C_ A /\ G = ( y e. A |-> if ( y e. S , C , B ) ) ) ) )
91 prex 
 |-  { B , C } e. _V
92 elmapg 
 |-  ( ( { B , C } e. _V /\ A e. V ) -> ( G e. ( { B , C } ^m A ) <-> G : A --> { B , C } ) )
93 91 1 92 sylancr 
 |-  ( ph -> ( G e. ( { B , C } ^m A ) <-> G : A --> { B , C } ) )
94 93 anbi1d 
 |-  ( ph -> ( ( G e. ( { B , C } ^m A ) /\ S = ( `' G " { C } ) ) <-> ( G : A --> { B , C } /\ S = ( `' G " { C } ) ) ) )
95 82 90 94 3bitr4d 
 |-  ( ph -> ( ( S e. ~P A /\ G = ( z e. A |-> if ( z e. S , C , B ) ) ) <-> ( G e. ( { B , C } ^m A ) /\ S = ( `' G " { C } ) ) ) )