Metamath Proof Explorer

Theorem wemapwe

Description: Construct lexicographic order on a function space based on a reverse well-ordering of the indices and a well-ordering of the values. (Contributed by Mario Carneiro, 29-May-2015) (Revised by AV, 3-Jul-2019)

Ref Expression
Hypotheses wemapwe.t 
|- T = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) }
wemapwe.u 
|- U = { x e. ( B ^m A ) | x finSupp Z }
wemapwe.2 
|- ( ph -> R We A )
wemapwe.3 
|- ( ph -> S We B )
wemapwe.4 
|- ( ph -> B =/= (/) )
wemapwe.5 
|- F = OrdIso ( R , A )
wemapwe.6 
|- G = OrdIso ( S , B )
wemapwe.7 
|- Z = ( G ` (/) )
Assertion wemapwe 
|- ( ph -> T We U )

Proof

Step Hyp Ref Expression
1 wemapwe.t 
 |-  T = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) }
2 wemapwe.u 
 |-  U = { x e. ( B ^m A ) | x finSupp Z }
3 wemapwe.2 
 |-  ( ph -> R We A )
4 wemapwe.3 
 |-  ( ph -> S We B )
5 wemapwe.4 
 |-  ( ph -> B =/= (/) )
6 wemapwe.5 
 |-  F = OrdIso ( R , A )
7 wemapwe.6 
 |-  G = OrdIso ( S , B )
8 wemapwe.7 
 |-  Z = ( G ` (/) )
9 eqid 
 |-  { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } = { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) }
10 eqid 
 |-  ( `' G ` Z ) = ( `' G ` Z )
11 simprr 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> A e. _V )
12 3 adantr 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> R We A )
13 6 oiiso 
 |-  ( ( A e. _V /\ R We A ) -> F Isom _E , R ( dom F , A ) )
14 11 12 13 syl2anc 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F Isom _E , R ( dom F , A ) )
15 isof1o 
 |-  ( F Isom _E , R ( dom F , A ) -> F : dom F -1-1-onto-> A )
16 14 15 syl 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F : dom F -1-1-onto-> A )
17 simprl 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> B e. _V )
18 4 adantr 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> S We B )
19 7 oiiso 
 |-  ( ( B e. _V /\ S We B ) -> G Isom _E , S ( dom G , B ) )
20 17 18 19 syl2anc 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G Isom _E , S ( dom G , B ) )
21 isof1o 
 |-  ( G Isom _E , S ( dom G , B ) -> G : dom G -1-1-onto-> B )
22 f1ocnv 
 |-  ( G : dom G -1-1-onto-> B -> `' G : B -1-1-onto-> dom G )
23 20 21 22 3syl 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> `' G : B -1-1-onto-> dom G )
24 6 oiexg 
 |-  ( A e. _V -> F e. _V )
25 24 ad2antll 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> F e. _V )
26 25 dmexd 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom F e. _V )
27 7 oiexg 
 |-  ( B e. _V -> G e. _V )
28 27 ad2antrl 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G e. _V )
29 28 dmexd 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G e. _V )
30 20 21 syl 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> G : dom G -1-1-onto-> B )
31 f1ofo 
 |-  ( G : dom G -1-1-onto-> B -> G : dom G -onto-> B )
32 forn 
 |-  ( G : dom G -onto-> B -> ran G = B )
33 30 31 32 3syl 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ran G = B )
34 5 adantr 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> B =/= (/) )
35 33 34 eqnetrd 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ran G =/= (/) )
36 dm0rn0 
 |-  ( dom G = (/) <-> ran G = (/) )
37 36 necon3bii 
 |-  ( dom G =/= (/) <-> ran G =/= (/) )
38 35 37 sylibr 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G =/= (/) )
39 7 oicl 
 |-  Ord dom G
40 ord0eln0 
 |-  ( Ord dom G -> ( (/) e. dom G <-> dom G =/= (/) ) )
41 39 40 ax-mp 
 |-  ( (/) e. dom G <-> dom G =/= (/) )
42 38 41 sylibr 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> (/) e. dom G )
43 7 oif 
 |-  G : dom G --> B
44 43 ffvelrni 
 |-  ( (/) e. dom G -> ( G ` (/) ) e. B )
45 42 44 syl 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( G ` (/) ) e. B )
46 8 45 eqeltrid 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> Z e. B )
47 2 9 10 16 23 11 17 26 29 46 mapfien 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } )
48 eqid 
 |-  { x e. ( dom G ^m dom F ) | x finSupp (/) } = { x e. ( dom G ^m dom F ) | x finSupp (/) }
49 7 oion 
 |-  ( B e. _V -> dom G e. On )
50 49 ad2antrl 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom G e. On )
51 6 oion 
 |-  ( A e. _V -> dom F e. On )
52 51 ad2antll 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom F e. On )
53 48 50 52 cantnfdm 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom ( dom G CNF dom F ) = { x e. ( dom G ^m dom F ) | x finSupp (/) } )
54 8 fveq2i 
 |-  ( `' G ` Z ) = ( `' G ` ( G ` (/) ) )
55 f1ocnvfv1 
 |-  ( ( G : dom G -1-1-onto-> B /\ (/) e. dom G ) -> ( `' G ` ( G ` (/) ) ) = (/) )
56 30 42 55 syl2anc 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` ( G ` (/) ) ) = (/) )
57 54 56 eqtrid 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( `' G ` Z ) = (/) )
58 57 breq2d 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( x finSupp ( `' G ` Z ) <-> x finSupp (/) ) )
59 58 rabbidv 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } = { x e. ( dom G ^m dom F ) | x finSupp (/) } )
60 53 59 eqtr4d 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> dom ( dom G CNF dom F ) = { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } )
61 60 f1oeq3d 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> dom ( dom G CNF dom F ) <-> ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> { x e. ( dom G ^m dom F ) | x finSupp ( `' G ` Z ) } ) )
62 47 61 mpbird 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> dom ( dom G CNF dom F ) )
63 eqid 
 |-  dom ( dom G CNF dom F ) = dom ( dom G CNF dom F )
64 eqid 
 |-  { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } = { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) }
65 63 50 52 64 oemapwe 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } We dom ( dom G CNF dom F ) /\ dom OrdIso ( { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } , dom ( dom G CNF dom F ) ) = ( dom G ^o dom F ) ) )
66 65 simpld 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } We dom ( dom G CNF dom F ) )
67 eqid 
 |-  { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } = { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) }
68 67 f1owe 
 |-  ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) : U -1-1-onto-> dom ( dom G CNF dom F ) -> ( { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } We dom ( dom G CNF dom F ) -> { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } We U ) )
69 62 66 68 sylc 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } We U )
70 weinxp 
 |-  ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } We U <-> ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) We U )
71 69 70 sylib 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) We U )
72 16 adantr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F : dom F -1-1-onto-> A )
73 f1ofn 
 |-  ( F : dom F -1-1-onto-> A -> F Fn dom F )
74 fveq2 
 |-  ( z = ( F ` c ) -> ( x ` z ) = ( x ` ( F ` c ) ) )
75 fveq2 
 |-  ( z = ( F ` c ) -> ( y ` z ) = ( y ` ( F ` c ) ) )
76 74 75 breq12d 
 |-  ( z = ( F ` c ) -> ( ( x ` z ) S ( y ` z ) <-> ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) ) )
77 breq1 
 |-  ( z = ( F ` c ) -> ( z R w <-> ( F ` c ) R w ) )
78 77 imbi1d 
 |-  ( z = ( F ` c ) -> ( ( z R w -> ( x ` w ) = ( y ` w ) ) <-> ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) )
79 78 ralbidv 
 |-  ( z = ( F ` c ) -> ( A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) )
80 76 79 anbi12d 
 |-  ( z = ( F ` c ) -> ( ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) ) )
81 80 rexrn 
 |-  ( F Fn dom F -> ( E. z e. ran F ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> E. c e. dom F ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) ) )
82 72 73 81 3syl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. z e. ran F ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> E. c e. dom F ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) ) )
83 f1ofo 
 |-  ( F : dom F -1-1-onto-> A -> F : dom F -onto-> A )
84 forn 
 |-  ( F : dom F -onto-> A -> ran F = A )
85 72 83 84 3syl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ran F = A )
86 85 rexeqdv 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. z e. ran F ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) ) )
87 28 adantr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> G e. _V )
88 cnvexg 
 |-  ( G e. _V -> `' G e. _V )
89 87 88 syl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> `' G e. _V )
90 vex 
 |-  x e. _V
91 25 adantr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F e. _V )
92 coexg 
 |-  ( ( x e. _V /\ F e. _V ) -> ( x o. F ) e. _V )
93 90 91 92 sylancr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( x o. F ) e. _V )
94 coexg 
 |-  ( ( `' G e. _V /\ ( x o. F ) e. _V ) -> ( `' G o. ( x o. F ) ) e. _V )
95 89 93 94 syl2anc 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( x o. F ) ) e. _V )
96 vex 
 |-  y e. _V
97 coexg 
 |-  ( ( y e. _V /\ F e. _V ) -> ( y o. F ) e. _V )
98 96 91 97 sylancr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( y o. F ) e. _V )
99 coexg 
 |-  ( ( `' G e. _V /\ ( y o. F ) e. _V ) -> ( `' G o. ( y o. F ) ) e. _V )
100 89 98 99 syl2anc 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( y o. F ) ) e. _V )
101 fveq1 
 |-  ( a = ( `' G o. ( x o. F ) ) -> ( a ` c ) = ( ( `' G o. ( x o. F ) ) ` c ) )
102 fveq1 
 |-  ( b = ( `' G o. ( y o. F ) ) -> ( b ` c ) = ( ( `' G o. ( y o. F ) ) ` c ) )
103 eleq12 
 |-  ( ( ( a ` c ) = ( ( `' G o. ( x o. F ) ) ` c ) /\ ( b ` c ) = ( ( `' G o. ( y o. F ) ) ` c ) ) -> ( ( a ` c ) e. ( b ` c ) <-> ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) ) )
104 101 102 103 syl2an 
 |-  ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( ( a ` c ) e. ( b ` c ) <-> ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) ) )
105 fveq1 
 |-  ( a = ( `' G o. ( x o. F ) ) -> ( a ` d ) = ( ( `' G o. ( x o. F ) ) ` d ) )
106 fveq1 
 |-  ( b = ( `' G o. ( y o. F ) ) -> ( b ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) )
107 105 106 eqeqan12d 
 |-  ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( ( a ` d ) = ( b ` d ) <-> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) )
108 107 imbi2d 
 |-  ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( ( c e. d -> ( a ` d ) = ( b ` d ) ) <-> ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) )
109 108 ralbidv 
 |-  ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) <-> A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) )
110 104 109 anbi12d 
 |-  ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) <-> ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
111 110 rexbidv 
 |-  ( ( a = ( `' G o. ( x o. F ) ) /\ b = ( `' G o. ( y o. F ) ) ) -> ( E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) <-> E. c e. dom F ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
112 111 64 brabga 
 |-  ( ( ( `' G o. ( x o. F ) ) e. _V /\ ( `' G o. ( y o. F ) ) e. _V ) -> ( ( `' G o. ( x o. F ) ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( `' G o. ( y o. F ) ) <-> E. c e. dom F ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
113 95 100 112 syl2anc 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( ( `' G o. ( x o. F ) ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( `' G o. ( y o. F ) ) <-> E. c e. dom F ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
114 eqid 
 |-  ( f e. U |-> ( `' G o. ( f o. F ) ) ) = ( f e. U |-> ( `' G o. ( f o. F ) ) )
115 coeq1 
 |-  ( f = x -> ( f o. F ) = ( x o. F ) )
116 115 coeq2d 
 |-  ( f = x -> ( `' G o. ( f o. F ) ) = ( `' G o. ( x o. F ) ) )
117 simprl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. U )
118 114 116 117 95 fvmptd3 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) = ( `' G o. ( x o. F ) ) )
119 coeq1 
 |-  ( f = y -> ( f o. F ) = ( y o. F ) )
120 119 coeq2d 
 |-  ( f = y -> ( `' G o. ( f o. F ) ) = ( `' G o. ( y o. F ) ) )
121 simprr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. U )
122 114 120 121 100 fvmptd3 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) = ( `' G o. ( y o. F ) ) )
123 118 122 breq12d 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) <-> ( `' G o. ( x o. F ) ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( `' G o. ( y o. F ) ) ) )
124 20 ad2antrr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> G Isom _E , S ( dom G , B ) )
125 isocnv 
 |-  ( G Isom _E , S ( dom G , B ) -> `' G Isom S , _E ( B , dom G ) )
126 124 125 syl 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> `' G Isom S , _E ( B , dom G ) )
127 2 ssrab3 
 |-  U C_ ( B ^m A )
128 127 117 sselid 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. ( B ^m A ) )
129 elmapi 
 |-  ( x e. ( B ^m A ) -> x : A --> B )
130 128 129 syl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x : A --> B )
131 6 oif 
 |-  F : dom F --> A
132 131 ffvelrni 
 |-  ( c e. dom F -> ( F ` c ) e. A )
133 ffvelrn 
 |-  ( ( x : A --> B /\ ( F ` c ) e. A ) -> ( x ` ( F ` c ) ) e. B )
134 130 132 133 syl2an 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( x ` ( F ` c ) ) e. B )
135 127 121 sselid 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. ( B ^m A ) )
136 elmapi 
 |-  ( y e. ( B ^m A ) -> y : A --> B )
137 135 136 syl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y : A --> B )
138 ffvelrn 
 |-  ( ( y : A --> B /\ ( F ` c ) e. A ) -> ( y ` ( F ` c ) ) e. B )
139 137 132 138 syl2an 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( y ` ( F ` c ) ) e. B )
140 isorel 
 |-  ( ( `' G Isom S , _E ( B , dom G ) /\ ( ( x ` ( F ` c ) ) e. B /\ ( y ` ( F ` c ) ) e. B ) ) -> ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) _E ( `' G ` ( y ` ( F ` c ) ) ) ) )
141 126 134 139 140 syl12anc 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) _E ( `' G ` ( y ` ( F ` c ) ) ) ) )
142 fvex 
 |-  ( `' G ` ( y ` ( F ` c ) ) ) e. _V
143 142 epeli 
 |-  ( ( `' G ` ( x ` ( F ` c ) ) ) _E ( `' G ` ( y ` ( F ` c ) ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) e. ( `' G ` ( y ` ( F ` c ) ) ) )
144 141 143 bitrdi 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) e. ( `' G ` ( y ` ( F ` c ) ) ) ) )
145 130 adantr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> x : A --> B )
146 fco 
 |-  ( ( x : A --> B /\ F : dom F --> A ) -> ( x o. F ) : dom F --> B )
147 145 131 146 sylancl 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( x o. F ) : dom F --> B )
148 fvco3 
 |-  ( ( ( x o. F ) : dom F --> B /\ c e. dom F ) -> ( ( `' G o. ( x o. F ) ) ` c ) = ( `' G ` ( ( x o. F ) ` c ) ) )
149 147 148 sylancom 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( `' G o. ( x o. F ) ) ` c ) = ( `' G ` ( ( x o. F ) ` c ) ) )
150 simpr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> c e. dom F )
151 fvco3 
 |-  ( ( F : dom F --> A /\ c e. dom F ) -> ( ( x o. F ) ` c ) = ( x ` ( F ` c ) ) )
152 131 150 151 sylancr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( x o. F ) ` c ) = ( x ` ( F ` c ) ) )
153 152 fveq2d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( `' G ` ( ( x o. F ) ` c ) ) = ( `' G ` ( x ` ( F ` c ) ) ) )
154 149 153 eqtrd 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( `' G o. ( x o. F ) ) ` c ) = ( `' G ` ( x ` ( F ` c ) ) ) )
155 137 adantr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> y : A --> B )
156 fco 
 |-  ( ( y : A --> B /\ F : dom F --> A ) -> ( y o. F ) : dom F --> B )
157 155 131 156 sylancl 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( y o. F ) : dom F --> B )
158 fvco3 
 |-  ( ( ( y o. F ) : dom F --> B /\ c e. dom F ) -> ( ( `' G o. ( y o. F ) ) ` c ) = ( `' G ` ( ( y o. F ) ` c ) ) )
159 157 158 sylancom 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( `' G o. ( y o. F ) ) ` c ) = ( `' G ` ( ( y o. F ) ` c ) ) )
160 fvco3 
 |-  ( ( F : dom F --> A /\ c e. dom F ) -> ( ( y o. F ) ` c ) = ( y ` ( F ` c ) ) )
161 131 150 160 sylancr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( y o. F ) ` c ) = ( y ` ( F ` c ) ) )
162 161 fveq2d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( `' G ` ( ( y o. F ) ` c ) ) = ( `' G ` ( y ` ( F ` c ) ) ) )
163 159 162 eqtrd 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( `' G o. ( y o. F ) ) ` c ) = ( `' G ` ( y ` ( F ` c ) ) ) )
164 154 163 eleq12d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) <-> ( `' G ` ( x ` ( F ` c ) ) ) e. ( `' G ` ( y ` ( F ` c ) ) ) ) )
165 144 164 bitr4d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) <-> ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) ) )
166 85 raleqdv 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( A. w e. ran F ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) )
167 breq2 
 |-  ( w = ( F ` d ) -> ( ( F ` c ) R w <-> ( F ` c ) R ( F ` d ) ) )
168 fveq2 
 |-  ( w = ( F ` d ) -> ( x ` w ) = ( x ` ( F ` d ) ) )
169 fveq2 
 |-  ( w = ( F ` d ) -> ( y ` w ) = ( y ` ( F ` d ) ) )
170 168 169 eqeq12d 
 |-  ( w = ( F ` d ) -> ( ( x ` w ) = ( y ` w ) <-> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) )
171 167 170 imbi12d 
 |-  ( w = ( F ` d ) -> ( ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
172 171 ralrn 
 |-  ( F Fn dom F -> ( A. w e. ran F ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
173 72 73 172 3syl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( A. w e. ran F ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
174 166 173 bitr3d 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
175 174 adantr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
176 epel 
 |-  ( c _E d <-> c e. d )
177 14 ad2antrr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> F Isom _E , R ( dom F , A ) )
178 isorel 
 |-  ( ( F Isom _E , R ( dom F , A ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( c _E d <-> ( F ` c ) R ( F ` d ) ) )
179 177 178 sylancom 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( c _E d <-> ( F ` c ) R ( F ` d ) ) )
180 176 179 bitr3id 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( c e. d <-> ( F ` c ) R ( F ` d ) ) )
181 147 adantrr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( x o. F ) : dom F --> B )
182 simprr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> d e. dom F )
183 181 182 fvco3d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( `' G o. ( x o. F ) ) ` d ) = ( `' G ` ( ( x o. F ) ` d ) ) )
184 157 adantrr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( y o. F ) : dom F --> B )
185 184 182 fvco3d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( `' G o. ( y o. F ) ) ` d ) = ( `' G ` ( ( y o. F ) ` d ) ) )
186 183 185 eqeq12d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) <-> ( `' G ` ( ( x o. F ) ` d ) ) = ( `' G ` ( ( y o. F ) ` d ) ) ) )
187 30 ad2antrr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> G : dom G -1-1-onto-> B )
188 f1of1 
 |-  ( `' G : B -1-1-onto-> dom G -> `' G : B -1-1-> dom G )
189 187 22 188 3syl 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> `' G : B -1-1-> dom G )
190 181 182 ffvelrnd 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( x o. F ) ` d ) e. B )
191 184 182 ffvelrnd 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( y o. F ) ` d ) e. B )
192 f1fveq 
 |-  ( ( `' G : B -1-1-> dom G /\ ( ( ( x o. F ) ` d ) e. B /\ ( ( y o. F ) ` d ) e. B ) ) -> ( ( `' G ` ( ( x o. F ) ` d ) ) = ( `' G ` ( ( y o. F ) ` d ) ) <-> ( ( x o. F ) ` d ) = ( ( y o. F ) ` d ) ) )
193 189 190 191 192 syl12anc 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( `' G ` ( ( x o. F ) ` d ) ) = ( `' G ` ( ( y o. F ) ` d ) ) <-> ( ( x o. F ) ` d ) = ( ( y o. F ) ` d ) ) )
194 fvco3 
 |-  ( ( F : dom F --> A /\ d e. dom F ) -> ( ( x o. F ) ` d ) = ( x ` ( F ` d ) ) )
195 131 182 194 sylancr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( x o. F ) ` d ) = ( x ` ( F ` d ) ) )
196 fvco3 
 |-  ( ( F : dom F --> A /\ d e. dom F ) -> ( ( y o. F ) ` d ) = ( y ` ( F ` d ) ) )
197 131 182 196 sylancr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( y o. F ) ` d ) = ( y ` ( F ` d ) ) )
198 195 197 eqeq12d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( ( x o. F ) ` d ) = ( ( y o. F ) ` d ) <-> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) )
199 186 193 198 3bitrd 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) <-> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) )
200 180 199 imbi12d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) <-> ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
201 200 anassrs 
 |-  ( ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) /\ d e. dom F ) -> ( ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) <-> ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
202 201 ralbidva 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) <-> A. d e. dom F ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
203 175 202 bitr4d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) )
204 165 203 anbi12d 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
205 204 rexbidva 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. c e. dom F ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) <-> E. c e. dom F ( ( ( `' G o. ( x o. F ) ) ` c ) e. ( ( `' G o. ( y o. F ) ) ` c ) /\ A. d e. dom F ( c e. d -> ( ( `' G o. ( x o. F ) ) ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) ) ) ) )
206 113 123 205 3bitr4rd 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. c e. dom F ( ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) /\ A. w e. A ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) ) )
207 82 86 206 3bitr3d 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) ) )
208 207 ex 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( ( x e. U /\ y e. U ) -> ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) ) ) )
209 208 pm5.32rd 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) /\ ( x e. U /\ y e. U ) ) <-> ( ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) /\ ( x e. U /\ y e. U ) ) ) )
210 209 opabbidv 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> { <. x , y >. | ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) /\ ( x e. U /\ y e. U ) ) } = { <. x , y >. | ( ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) /\ ( x e. U /\ y e. U ) ) } )
211 df-xp 
 |-  ( U X. U ) = { <. x , y >. | ( x e. U /\ y e. U ) }
212 1 211 ineq12i 
 |-  ( T i^i ( U X. U ) ) = ( { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) } i^i { <. x , y >. | ( x e. U /\ y e. U ) } )
213 inopab 
 |-  ( { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) } i^i { <. x , y >. | ( x e. U /\ y e. U ) } ) = { <. x , y >. | ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) /\ ( x e. U /\ y e. U ) ) }
214 212 213 eqtri 
 |-  ( T i^i ( U X. U ) ) = { <. x , y >. | ( E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( z R w -> ( x ` w ) = ( y ` w ) ) ) /\ ( x e. U /\ y e. U ) ) }
215 211 ineq2i 
 |-  ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) = ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i { <. x , y >. | ( x e. U /\ y e. U ) } )
216 inopab 
 |-  ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i { <. x , y >. | ( x e. U /\ y e. U ) } ) = { <. x , y >. | ( ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) /\ ( x e. U /\ y e. U ) ) }
217 215 216 eqtri 
 |-  ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) = { <. x , y >. | ( ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) /\ ( x e. U /\ y e. U ) ) }
218 210 214 217 3eqtr4g 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( T i^i ( U X. U ) ) = ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) )
219 weeq1 
 |-  ( ( T i^i ( U X. U ) ) = ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) -> ( ( T i^i ( U X. U ) ) We U <-> ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) We U ) )
220 218 219 syl 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( ( T i^i ( U X. U ) ) We U <-> ( { <. x , y >. | ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` x ) { <. a , b >. | E. c e. dom F ( ( a ` c ) e. ( b ` c ) /\ A. d e. dom F ( c e. d -> ( a ` d ) = ( b ` d ) ) ) } ( ( f e. U |-> ( `' G o. ( f o. F ) ) ) ` y ) } i^i ( U X. U ) ) We U ) )
221 71 220 mpbird 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( T i^i ( U X. U ) ) We U )
222 weinxp 
 |-  ( T We U <-> ( T i^i ( U X. U ) ) We U )
223 221 222 sylibr 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> T We U )
224 223 ex 
 |-  ( ph -> ( ( B e. _V /\ A e. _V ) -> T We U ) )
225 we0 
 |-  T We (/)
226 elmapex 
 |-  ( x e. ( B ^m A ) -> ( B e. _V /\ A e. _V ) )
227 226 con3i 
 |-  ( -. ( B e. _V /\ A e. _V ) -> -. x e. ( B ^m A ) )
228 227 pm2.21d 
 |-  ( -. ( B e. _V /\ A e. _V ) -> ( x e. ( B ^m A ) -> -. x finSupp Z ) )
229 228 ralrimiv 
 |-  ( -. ( B e. _V /\ A e. _V ) -> A. x e. ( B ^m A ) -. x finSupp Z )
230 rabeq0 
 |-  ( { x e. ( B ^m A ) | x finSupp Z } = (/) <-> A. x e. ( B ^m A ) -. x finSupp Z )
231 229 230 sylibr 
 |-  ( -. ( B e. _V /\ A e. _V ) -> { x e. ( B ^m A ) | x finSupp Z } = (/) )
232 2 231 eqtrid 
 |-  ( -. ( B e. _V /\ A e. _V ) -> U = (/) )
233 weeq2 
 |-  ( U = (/) -> ( T We U <-> T We (/) ) )
234 232 233 syl 
 |-  ( -. ( B e. _V /\ A e. _V ) -> ( T We U <-> T We (/) ) )
235 225 234 mpbiri 
 |-  ( -. ( B e. _V /\ A e. _V ) -> T We U )
236 224 235 pm2.61d1 
 |-  ( ph -> T We U )