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 ffvelrnda
 |-  ( ( ( 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 } ) ) ) )