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 >. | E. z e. A ( ( z e. y /\ -. z e. x ) /\ A. w e. A ( w R z -> ( w e. x <-> w e. y ) ) ) }
wepwso.u 
|- U = { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) }
wepwso.f 
|- F = ( a e. ( 2o ^m A ) |-> ( `' a " { 1o } ) )
Assertion wepwsolem 
|- ( A e. _V -> F Isom U , T ( ( 2o ^m A ) , ~P A ) )

Proof

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