Metamath Proof Explorer


Theorem wepwsolem

Description: Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses wepwso.t T=xy|zAzy¬zxwAwRzwxwy
wepwso.u U=xy|zAxzEyzwAwRzxw=yw
wepwso.f F=a2𝑜Aa-11𝑜
Assertion wepwsolem AVFIsomU,T2𝑜A𝒫A

Proof

Step Hyp Ref Expression
1 wepwso.t T=xy|zAzy¬zxwAwRzwxwy
2 wepwso.u U=xy|zAxzEyzwAwRzxw=yw
3 wepwso.f F=a2𝑜Aa-11𝑜
4 3 pw2f1o2 AVF:2𝑜A1-1 onto𝒫A
5 fvex czV
6 5 epeli bzEczbzcz
7 elmapi b2𝑜Ab:A2𝑜
8 7 ad2antrl AVb2𝑜Ac2𝑜Ab:A2𝑜
9 8 ffvelrnda AVb2𝑜Ac2𝑜AzAbz2𝑜
10 elmapi c2𝑜Ac:A2𝑜
11 10 ad2antll AVb2𝑜Ac2𝑜Ac:A2𝑜
12 11 ffvelrnda AVb2𝑜Ac2𝑜AzAcz2𝑜
13 n0i bzcz¬cz=
14 13 adantl bz2𝑜cz2𝑜bzcz¬cz=
15 elpri cz1𝑜cz=cz=1𝑜
16 df2o3 2𝑜=1𝑜
17 15 16 eleq2s cz2𝑜cz=cz=1𝑜
18 17 ad2antlr bz2𝑜cz2𝑜bzczcz=cz=1𝑜
19 orel1 ¬cz=cz=cz=1𝑜cz=1𝑜
20 14 18 19 sylc bz2𝑜cz2𝑜bzczcz=1𝑜
21 1on 1𝑜On
22 21 onirri ¬1𝑜1𝑜
23 eleq12 bz=1𝑜cz=1𝑜bzcz1𝑜1𝑜
24 23 biimpd bz=1𝑜cz=1𝑜bzcz1𝑜1𝑜
25 24 expcom cz=1𝑜bz=1𝑜bzcz1𝑜1𝑜
26 25 com3r bzczcz=1𝑜bz=1𝑜1𝑜1𝑜
27 26 imp bzczcz=1𝑜bz=1𝑜1𝑜1𝑜
28 27 adantll bz2𝑜cz2𝑜bzczcz=1𝑜bz=1𝑜1𝑜1𝑜
29 22 28 mtoi bz2𝑜cz2𝑜bzczcz=1𝑜¬bz=1𝑜
30 20 29 mpdan bz2𝑜cz2𝑜bzcz¬bz=1𝑜
31 20 30 jca bz2𝑜cz2𝑜bzczcz=1𝑜¬bz=1𝑜
32 elpri bz1𝑜bz=bz=1𝑜
33 32 16 eleq2s bz2𝑜bz=bz=1𝑜
34 33 adantr bz2𝑜cz2𝑜bz=bz=1𝑜
35 orel2 ¬bz=1𝑜bz=bz=1𝑜bz=
36 34 35 mpan9 bz2𝑜cz2𝑜¬bz=1𝑜bz=
37 36 adantrl bz2𝑜cz2𝑜cz=1𝑜¬bz=1𝑜bz=
38 0lt1o 1𝑜
39 37 38 eqeltrdi bz2𝑜cz2𝑜cz=1𝑜¬bz=1𝑜bz1𝑜
40 simprl bz2𝑜cz2𝑜cz=1𝑜¬bz=1𝑜cz=1𝑜
41 39 40 eleqtrrd bz2𝑜cz2𝑜cz=1𝑜¬bz=1𝑜bzcz
42 31 41 impbida bz2𝑜cz2𝑜bzczcz=1𝑜¬bz=1𝑜
43 9 12 42 syl2anc AVb2𝑜Ac2𝑜AzAbzczcz=1𝑜¬bz=1𝑜
44 simplrr AVb2𝑜Ac2𝑜AzAc2𝑜A
45 3 pw2f1o2val2 c2𝑜AzAzFccz=1𝑜
46 44 45 sylancom AVb2𝑜Ac2𝑜AzAzFccz=1𝑜
47 simplrl AVb2𝑜Ac2𝑜AzAb2𝑜A
48 3 pw2f1o2val2 b2𝑜AzAzFbbz=1𝑜
49 47 48 sylancom AVb2𝑜Ac2𝑜AzAzFbbz=1𝑜
50 49 notbid AVb2𝑜Ac2𝑜AzA¬zFb¬bz=1𝑜
51 46 50 anbi12d AVb2𝑜Ac2𝑜AzAzFc¬zFbcz=1𝑜¬bz=1𝑜
52 43 51 bitr4d AVb2𝑜Ac2𝑜AzAbzczzFc¬zFb
53 6 52 syl5bb AVb2𝑜Ac2𝑜AzAbzEczzFc¬zFb
54 8 ffvelrnda AVb2𝑜Ac2𝑜AwAbw2𝑜
55 11 ffvelrnda AVb2𝑜Ac2𝑜AwAcw2𝑜
56 eqeq1 bw=cwbw=1𝑜cw=1𝑜
57 simplr bw2𝑜cw2𝑜bw=bw=1𝑜cw=1𝑜bw=
58 1n0 1𝑜
59 58 nesymi ¬=1𝑜
60 eqeq1 bw=bw=1𝑜=1𝑜
61 59 60 mtbiri bw=¬bw=1𝑜
62 61 ad2antlr bw2𝑜cw2𝑜bw=bw=1𝑜cw=1𝑜¬bw=1𝑜
63 simpr bw2𝑜cw2𝑜bw=bw=1𝑜cw=1𝑜bw=1𝑜cw=1𝑜
64 62 63 mtbid bw2𝑜cw2𝑜bw=bw=1𝑜cw=1𝑜¬cw=1𝑜
65 elpri cw1𝑜cw=cw=1𝑜
66 65 16 eleq2s cw2𝑜cw=cw=1𝑜
67 66 ad3antlr bw2𝑜cw2𝑜bw=bw=1𝑜cw=1𝑜cw=cw=1𝑜
68 orel2 ¬cw=1𝑜cw=cw=1𝑜cw=
69 64 67 68 sylc bw2𝑜cw2𝑜bw=bw=1𝑜cw=1𝑜cw=
70 57 69 eqtr4d bw2𝑜cw2𝑜bw=bw=1𝑜cw=1𝑜bw=cw
71 70 ex bw2𝑜cw2𝑜bw=bw=1𝑜cw=1𝑜bw=cw
72 simplr bw2𝑜cw2𝑜bw=1𝑜bw=1𝑜cw=1𝑜bw=1𝑜
73 simpr bw2𝑜cw2𝑜bw=1𝑜bw=1𝑜cw=1𝑜bw=1𝑜cw=1𝑜
74 72 73 mpbid bw2𝑜cw2𝑜bw=1𝑜bw=1𝑜cw=1𝑜cw=1𝑜
75 72 74 eqtr4d bw2𝑜cw2𝑜bw=1𝑜bw=1𝑜cw=1𝑜bw=cw
76 75 ex bw2𝑜cw2𝑜bw=1𝑜bw=1𝑜cw=1𝑜bw=cw
77 elpri bw1𝑜bw=bw=1𝑜
78 77 16 eleq2s bw2𝑜bw=bw=1𝑜
79 78 adantr bw2𝑜cw2𝑜bw=bw=1𝑜
80 71 76 79 mpjaodan bw2𝑜cw2𝑜bw=1𝑜cw=1𝑜bw=cw
81 56 80 impbid2 bw2𝑜cw2𝑜bw=cwbw=1𝑜cw=1𝑜
82 54 55 81 syl2anc AVb2𝑜Ac2𝑜AwAbw=cwbw=1𝑜cw=1𝑜
83 simplrl AVb2𝑜Ac2𝑜AwAb2𝑜A
84 3 pw2f1o2val2 b2𝑜AwAwFbbw=1𝑜
85 83 84 sylancom AVb2𝑜Ac2𝑜AwAwFbbw=1𝑜
86 simplrr AVb2𝑜Ac2𝑜AwAc2𝑜A
87 3 pw2f1o2val2 c2𝑜AwAwFccw=1𝑜
88 86 87 sylancom AVb2𝑜Ac2𝑜AwAwFccw=1𝑜
89 85 88 bibi12d AVb2𝑜Ac2𝑜AwAwFbwFcbw=1𝑜cw=1𝑜
90 82 89 bitr4d AVb2𝑜Ac2𝑜AwAbw=cwwFbwFc
91 90 imbi2d AVb2𝑜Ac2𝑜AwAwRzbw=cwwRzwFbwFc
92 91 ralbidva AVb2𝑜Ac2𝑜AwAwRzbw=cwwAwRzwFbwFc
93 92 adantr AVb2𝑜Ac2𝑜AzAwAwRzbw=cwwAwRzwFbwFc
94 53 93 anbi12d AVb2𝑜Ac2𝑜AzAbzEczwAwRzbw=cwzFc¬zFbwAwRzwFbwFc
95 94 rexbidva AVb2𝑜Ac2𝑜AzAbzEczwAwRzbw=cwzAzFc¬zFbwAwRzwFbwFc
96 vex bV
97 vex cV
98 fveq1 x=bxz=bz
99 fveq1 y=cyz=cz
100 98 99 breqan12d x=by=cxzEyzbzEcz
101 fveq1 x=bxw=bw
102 fveq1 y=cyw=cw
103 101 102 eqeqan12d x=by=cxw=ywbw=cw
104 103 imbi2d x=by=cwRzxw=ywwRzbw=cw
105 104 ralbidv x=by=cwAwRzxw=ywwAwRzbw=cw
106 100 105 anbi12d x=by=cxzEyzwAwRzxw=ywbzEczwAwRzbw=cw
107 106 rexbidv x=by=czAxzEyzwAwRzxw=ywzAbzEczwAwRzbw=cw
108 96 97 107 2 braba bUczAbzEczwAwRzbw=cw
109 fvex FbV
110 fvex FcV
111 eleq2 y=FczyzFc
112 eleq2 x=FbzxzFb
113 112 notbid x=Fb¬zx¬zFb
114 111 113 bi2anan9r x=Fby=Fczy¬zxzFc¬zFb
115 eleq2 x=FbwxwFb
116 eleq2 y=FcwywFc
117 115 116 bi2bian9 x=Fby=FcwxwywFbwFc
118 117 imbi2d x=Fby=FcwRzwxwywRzwFbwFc
119 118 ralbidv x=Fby=FcwAwRzwxwywAwRzwFbwFc
120 114 119 anbi12d x=Fby=Fczy¬zxwAwRzwxwyzFc¬zFbwAwRzwFbwFc
121 120 rexbidv x=Fby=FczAzy¬zxwAwRzwxwyzAzFc¬zFbwAwRzwFbwFc
122 109 110 121 1 braba FbTFczAzFc¬zFbwAwRzwFbwFc
123 95 108 122 3bitr4g AVb2𝑜Ac2𝑜AbUcFbTFc
124 123 ralrimivva AVb2𝑜Ac2𝑜AbUcFbTFc
125 df-isom FIsomU,T2𝑜A𝒫AF:2𝑜A1-1 onto𝒫Ab2𝑜Ac2𝑜AbUcFbTFc
126 4 124 125 sylanbrc AVFIsomU,T2𝑜A𝒫A