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 = x y | z A z y ¬ z x w A w R z w x w y
wepwso.u U = x y | z A x z E y z w A w R z x w = y w
wepwso.f F = a 2 𝑜 A a -1 1 𝑜
Assertion wepwsolem A V F Isom U , T 2 𝑜 A 𝒫 A

Proof

Step Hyp Ref Expression
1 wepwso.t T = x y | z A z y ¬ z x w A w R z w x w y
2 wepwso.u U = x y | z A x z E y z w A w R z x w = y w
3 wepwso.f F = a 2 𝑜 A a -1 1 𝑜
4 3 pw2f1o2 A V F : 2 𝑜 A 1-1 onto 𝒫 A
5 fvex c z V
6 5 epeli b z E c z b z c z
7 elmapi b 2 𝑜 A b : A 2 𝑜
8 7 ad2antrl A V b 2 𝑜 A c 2 𝑜 A b : A 2 𝑜
9 8 ffvelrnda A V b 2 𝑜 A c 2 𝑜 A z A b z 2 𝑜
10 elmapi c 2 𝑜 A c : A 2 𝑜
11 10 ad2antll A V b 2 𝑜 A c 2 𝑜 A c : A 2 𝑜
12 11 ffvelrnda A V b 2 𝑜 A c 2 𝑜 A z A c z 2 𝑜
13 n0i b z c z ¬ c z =
14 13 adantl b z 2 𝑜 c z 2 𝑜 b z c z ¬ c z =
15 elpri c z 1 𝑜 c z = c z = 1 𝑜
16 df2o3 2 𝑜 = 1 𝑜
17 15 16 eleq2s c z 2 𝑜 c z = c z = 1 𝑜
18 17 ad2antlr b z 2 𝑜 c z 2 𝑜 b z c z c z = c z = 1 𝑜
19 orel1 ¬ c z = c z = c z = 1 𝑜 c z = 1 𝑜
20 14 18 19 sylc b z 2 𝑜 c z 2 𝑜 b z c z c z = 1 𝑜
21 1on 1 𝑜 On
22 21 onirri ¬ 1 𝑜 1 𝑜
23 eleq12 b z = 1 𝑜 c z = 1 𝑜 b z c z 1 𝑜 1 𝑜
24 23 biimpd b z = 1 𝑜 c z = 1 𝑜 b z c z 1 𝑜 1 𝑜
25 24 expcom c z = 1 𝑜 b z = 1 𝑜 b z c z 1 𝑜 1 𝑜
26 25 com3r b z c z c z = 1 𝑜 b z = 1 𝑜 1 𝑜 1 𝑜
27 26 imp b z c z c z = 1 𝑜 b z = 1 𝑜 1 𝑜 1 𝑜
28 27 adantll b z 2 𝑜 c z 2 𝑜 b z c z c z = 1 𝑜 b z = 1 𝑜 1 𝑜 1 𝑜
29 22 28 mtoi b z 2 𝑜 c z 2 𝑜 b z c z c z = 1 𝑜 ¬ b z = 1 𝑜
30 20 29 mpdan b z 2 𝑜 c z 2 𝑜 b z c z ¬ b z = 1 𝑜
31 20 30 jca b z 2 𝑜 c z 2 𝑜 b z c z c z = 1 𝑜 ¬ b z = 1 𝑜
32 elpri b z 1 𝑜 b z = b z = 1 𝑜
33 32 16 eleq2s b z 2 𝑜 b z = b z = 1 𝑜
34 33 adantr b z 2 𝑜 c z 2 𝑜 b z = b z = 1 𝑜
35 orel2 ¬ b z = 1 𝑜 b z = b z = 1 𝑜 b z =
36 34 35 mpan9 b z 2 𝑜 c z 2 𝑜 ¬ b z = 1 𝑜 b z =
37 36 adantrl b z 2 𝑜 c z 2 𝑜 c z = 1 𝑜 ¬ b z = 1 𝑜 b z =
38 0lt1o 1 𝑜
39 37 38 eqeltrdi b z 2 𝑜 c z 2 𝑜 c z = 1 𝑜 ¬ b z = 1 𝑜 b z 1 𝑜
40 simprl b z 2 𝑜 c z 2 𝑜 c z = 1 𝑜 ¬ b z = 1 𝑜 c z = 1 𝑜
41 39 40 eleqtrrd b z 2 𝑜 c z 2 𝑜 c z = 1 𝑜 ¬ b z = 1 𝑜 b z c z
42 31 41 impbida b z 2 𝑜 c z 2 𝑜 b z c z c z = 1 𝑜 ¬ b z = 1 𝑜
43 9 12 42 syl2anc A V b 2 𝑜 A c 2 𝑜 A z A b z c z c z = 1 𝑜 ¬ b z = 1 𝑜
44 simplrr A V b 2 𝑜 A c 2 𝑜 A z A c 2 𝑜 A
45 3 pw2f1o2val2 c 2 𝑜 A z A z F c c z = 1 𝑜
46 44 45 sylancom A V b 2 𝑜 A c 2 𝑜 A z A z F c c z = 1 𝑜
47 simplrl A V b 2 𝑜 A c 2 𝑜 A z A b 2 𝑜 A
48 3 pw2f1o2val2 b 2 𝑜 A z A z F b b z = 1 𝑜
49 47 48 sylancom A V b 2 𝑜 A c 2 𝑜 A z A z F b b z = 1 𝑜
50 49 notbid A V b 2 𝑜 A c 2 𝑜 A z A ¬ z F b ¬ b z = 1 𝑜
51 46 50 anbi12d A V b 2 𝑜 A c 2 𝑜 A z A z F c ¬ z F b c z = 1 𝑜 ¬ b z = 1 𝑜
52 43 51 bitr4d A V b 2 𝑜 A c 2 𝑜 A z A b z c z z F c ¬ z F b
53 6 52 syl5bb A V b 2 𝑜 A c 2 𝑜 A z A b z E c z z F c ¬ z F b
54 8 ffvelrnda A V b 2 𝑜 A c 2 𝑜 A w A b w 2 𝑜
55 11 ffvelrnda A V b 2 𝑜 A c 2 𝑜 A w A c w 2 𝑜
56 eqeq1 b w = c w b w = 1 𝑜 c w = 1 𝑜
57 simplr b w 2 𝑜 c w 2 𝑜 b w = b w = 1 𝑜 c w = 1 𝑜 b w =
58 1n0 1 𝑜
59 58 nesymi ¬ = 1 𝑜
60 eqeq1 b w = b w = 1 𝑜 = 1 𝑜
61 59 60 mtbiri b w = ¬ b w = 1 𝑜
62 61 ad2antlr b w 2 𝑜 c w 2 𝑜 b w = b w = 1 𝑜 c w = 1 𝑜 ¬ b w = 1 𝑜
63 simpr b w 2 𝑜 c w 2 𝑜 b w = b w = 1 𝑜 c w = 1 𝑜 b w = 1 𝑜 c w = 1 𝑜
64 62 63 mtbid b w 2 𝑜 c w 2 𝑜 b w = b w = 1 𝑜 c w = 1 𝑜 ¬ c w = 1 𝑜
65 elpri c w 1 𝑜 c w = c w = 1 𝑜
66 65 16 eleq2s c w 2 𝑜 c w = c w = 1 𝑜
67 66 ad3antlr b w 2 𝑜 c w 2 𝑜 b w = b w = 1 𝑜 c w = 1 𝑜 c w = c w = 1 𝑜
68 orel2 ¬ c w = 1 𝑜 c w = c w = 1 𝑜 c w =
69 64 67 68 sylc b w 2 𝑜 c w 2 𝑜 b w = b w = 1 𝑜 c w = 1 𝑜 c w =
70 57 69 eqtr4d b w 2 𝑜 c w 2 𝑜 b w = b w = 1 𝑜 c w = 1 𝑜 b w = c w
71 70 ex b w 2 𝑜 c w 2 𝑜 b w = b w = 1 𝑜 c w = 1 𝑜 b w = c w
72 simplr b w 2 𝑜 c w 2 𝑜 b w = 1 𝑜 b w = 1 𝑜 c w = 1 𝑜 b w = 1 𝑜
73 simpr b w 2 𝑜 c w 2 𝑜 b w = 1 𝑜 b w = 1 𝑜 c w = 1 𝑜 b w = 1 𝑜 c w = 1 𝑜
74 72 73 mpbid b w 2 𝑜 c w 2 𝑜 b w = 1 𝑜 b w = 1 𝑜 c w = 1 𝑜 c w = 1 𝑜
75 72 74 eqtr4d b w 2 𝑜 c w 2 𝑜 b w = 1 𝑜 b w = 1 𝑜 c w = 1 𝑜 b w = c w
76 75 ex b w 2 𝑜 c w 2 𝑜 b w = 1 𝑜 b w = 1 𝑜 c w = 1 𝑜 b w = c w
77 elpri b w 1 𝑜 b w = b w = 1 𝑜
78 77 16 eleq2s b w 2 𝑜 b w = b w = 1 𝑜
79 78 adantr b w 2 𝑜 c w 2 𝑜 b w = b w = 1 𝑜
80 71 76 79 mpjaodan b w 2 𝑜 c w 2 𝑜 b w = 1 𝑜 c w = 1 𝑜 b w = c w
81 56 80 impbid2 b w 2 𝑜 c w 2 𝑜 b w = c w b w = 1 𝑜 c w = 1 𝑜
82 54 55 81 syl2anc A V b 2 𝑜 A c 2 𝑜 A w A b w = c w b w = 1 𝑜 c w = 1 𝑜
83 simplrl A V b 2 𝑜 A c 2 𝑜 A w A b 2 𝑜 A
84 3 pw2f1o2val2 b 2 𝑜 A w A w F b b w = 1 𝑜
85 83 84 sylancom A V b 2 𝑜 A c 2 𝑜 A w A w F b b w = 1 𝑜
86 simplrr A V b 2 𝑜 A c 2 𝑜 A w A c 2 𝑜 A
87 3 pw2f1o2val2 c 2 𝑜 A w A w F c c w = 1 𝑜
88 86 87 sylancom A V b 2 𝑜 A c 2 𝑜 A w A w F c c w = 1 𝑜
89 85 88 bibi12d A V b 2 𝑜 A c 2 𝑜 A w A w F b w F c b w = 1 𝑜 c w = 1 𝑜
90 82 89 bitr4d A V b 2 𝑜 A c 2 𝑜 A w A b w = c w w F b w F c
91 90 imbi2d A V b 2 𝑜 A c 2 𝑜 A w A w R z b w = c w w R z w F b w F c
92 91 ralbidva A V b 2 𝑜 A c 2 𝑜 A w A w R z b w = c w w A w R z w F b w F c
93 92 adantr A V b 2 𝑜 A c 2 𝑜 A z A w A w R z b w = c w w A w R z w F b w F c
94 53 93 anbi12d A V b 2 𝑜 A c 2 𝑜 A z A b z E c z w A w R z b w = c w z F c ¬ z F b w A w R z w F b w F c
95 94 rexbidva A V b 2 𝑜 A c 2 𝑜 A z A b z E c z w A w R z b w = c w z A z F c ¬ z F b w A w R z w F b w F c
96 vex b V
97 vex c V
98 fveq1 x = b x z = b z
99 fveq1 y = c y z = c z
100 98 99 breqan12d x = b y = c x z E y z b z E c z
101 fveq1 x = b x w = b w
102 fveq1 y = c y w = c w
103 101 102 eqeqan12d x = b y = c x w = y w b w = c w
104 103 imbi2d x = b y = c w R z x w = y w w R z b w = c w
105 104 ralbidv x = b y = c w A w R z x w = y w w A w R z b w = c w
106 100 105 anbi12d x = b y = c x z E y z w A w R z x w = y w b z E c z w A w R z b w = c w
107 106 rexbidv x = b y = c z A x z E y z w A w R z x w = y w z A b z E c z w A w R z b w = c w
108 96 97 107 2 braba b U c z A b z E c z w A w R z b w = c w
109 fvex F b V
110 fvex F c V
111 eleq2 y = F c z y z F c
112 eleq2 x = F b z x z F b
113 112 notbid x = F b ¬ z x ¬ z F b
114 111 113 bi2anan9r x = F b y = F c z y ¬ z x z F c ¬ z F b
115 eleq2 x = F b w x w F b
116 eleq2 y = F c w y w F c
117 115 116 bi2bian9 x = F b y = F c w x w y w F b w F c
118 117 imbi2d x = F b y = F c w R z w x w y w R z w F b w F c
119 118 ralbidv x = F b y = F c w A w R z w x w y w A w R z w F b w F c
120 114 119 anbi12d x = F b y = F c z y ¬ z x w A w R z w x w y z F c ¬ z F b w A w R z w F b w F c
121 120 rexbidv x = F b y = F c z A z y ¬ z x w A w R z w x w y z A z F c ¬ z F b w A w R z w F b w F c
122 109 110 121 1 braba F b T F c z A z F c ¬ z F b w A w R z w F b w F c
123 95 108 122 3bitr4g A V b 2 𝑜 A c 2 𝑜 A b U c F b T F c
124 123 ralrimivva A V b 2 𝑜 A c 2 𝑜 A b U c F b T F c
125 df-isom F Isom U , T 2 𝑜 A 𝒫 A F : 2 𝑜 A 1-1 onto 𝒫 A b 2 𝑜 A c 2 𝑜 A b U c F b T F c
126 4 124 125 sylanbrc A V F Isom U , T 2 𝑜 A 𝒫 A