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 ffvelcdmi 
 |-  ( (/) 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 ) -> ( { <. 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 <-> { <. 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 ) ) )
69 68 biimprd 
 |-  ( ( 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 ) )
70 62 66 69 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 )
71 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 )
72 70 71 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 )
73 16 adantr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F : dom F -1-1-onto-> A )
74 f1ofn 
 |-  ( F : dom F -1-1-onto-> A -> F Fn dom F )
75 fveq2 
 |-  ( z = ( F ` c ) -> ( x ` z ) = ( x ` ( F ` c ) ) )
76 fveq2 
 |-  ( z = ( F ` c ) -> ( y ` z ) = ( y ` ( F ` c ) ) )
77 75 76 breq12d 
 |-  ( z = ( F ` c ) -> ( ( x ` z ) S ( y ` z ) <-> ( x ` ( F ` c ) ) S ( y ` ( F ` c ) ) ) )
78 breq1 
 |-  ( z = ( F ` c ) -> ( z R w <-> ( F ` c ) R w ) )
79 78 imbi1d 
 |-  ( z = ( F ` c ) -> ( ( z R w -> ( x ` w ) = ( y ` w ) ) <-> ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) ) )
80 79 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 ) ) ) )
81 77 80 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 ) ) ) ) )
82 81 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 ) ) ) ) )
83 73 74 82 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 ) ) ) ) )
84 f1ofo 
 |-  ( F : dom F -1-1-onto-> A -> F : dom F -onto-> A )
85 forn 
 |-  ( F : dom F -onto-> A -> ran F = A )
86 73 84 85 3syl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ran F = A )
87 86 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 ) ) ) ) )
88 28 adantr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> G e. _V )
89 cnvexg 
 |-  ( G e. _V -> `' G e. _V )
90 88 89 syl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> `' G e. _V )
91 vex 
 |-  x e. _V
92 25 adantr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> F e. _V )
93 coexg 
 |-  ( ( x e. _V /\ F e. _V ) -> ( x o. F ) e. _V )
94 91 92 93 sylancr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( x o. F ) e. _V )
95 90 94 coexd 
 |-  ( ( ( 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 92 97 sylancr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( y o. F ) e. _V )
99 90 98 coexd 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> ( `' G o. ( y o. F ) ) e. _V )
100 fveq1 
 |-  ( a = ( `' G o. ( x o. F ) ) -> ( a ` c ) = ( ( `' G o. ( x o. F ) ) ` c ) )
101 fveq1 
 |-  ( b = ( `' G o. ( y o. F ) ) -> ( b ` c ) = ( ( `' G o. ( y o. F ) ) ` c ) )
102 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 ) ) )
103 100 101 102 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 ) ) )
104 fveq1 
 |-  ( a = ( `' G o. ( x o. F ) ) -> ( a ` d ) = ( ( `' G o. ( x o. F ) ) ` d ) )
105 fveq1 
 |-  ( b = ( `' G o. ( y o. F ) ) -> ( b ` d ) = ( ( `' G o. ( y o. F ) ) ` d ) )
106 104 105 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 ) ) )
107 106 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 ) ) ) )
108 107 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 ) ) ) )
109 103 108 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 ) ) ) ) )
110 109 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 ) ) ) ) )
111 110 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 ) ) ) ) )
112 95 99 111 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 ) ) ) ) )
113 eqid 
 |-  ( f e. U |-> ( `' G o. ( f o. F ) ) ) = ( f e. U |-> ( `' G o. ( f o. F ) ) )
114 coeq1 
 |-  ( f = x -> ( f o. F ) = ( x o. F ) )
115 114 coeq2d 
 |-  ( f = x -> ( `' G o. ( f o. F ) ) = ( `' G o. ( x o. F ) ) )
116 simprl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. U )
117 113 115 116 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 ) ) )
118 coeq1 
 |-  ( f = y -> ( f o. F ) = ( y o. F ) )
119 118 coeq2d 
 |-  ( f = y -> ( `' G o. ( f o. F ) ) = ( `' G o. ( y o. F ) ) )
120 simprr 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. U )
121 113 119 120 99 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 ) ) )
122 117 121 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 ) ) ) )
123 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 ) )
124 isocnv 
 |-  ( G Isom _E , S ( dom G , B ) -> `' G Isom S , _E ( B , dom G ) )
125 123 124 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 ) )
126 2 ssrab3 
 |-  U C_ ( B ^m A )
127 126 116 sselid 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x e. ( B ^m A ) )
128 elmapi 
 |-  ( x e. ( B ^m A ) -> x : A --> B )
129 127 128 syl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> x : A --> B )
130 6 oif 
 |-  F : dom F --> A
131 130 ffvelcdmi 
 |-  ( c e. dom F -> ( F ` c ) e. A )
132 ffvelcdm 
 |-  ( ( x : A --> B /\ ( F ` c ) e. A ) -> ( x ` ( F ` c ) ) e. B )
133 129 131 132 syl2an 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( x ` ( F ` c ) ) e. B )
134 126 120 sselid 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y e. ( B ^m A ) )
135 elmapi 
 |-  ( y e. ( B ^m A ) -> y : A --> B )
136 134 135 syl 
 |-  ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) -> y : A --> B )
137 ffvelcdm 
 |-  ( ( y : A --> B /\ ( F ` c ) e. A ) -> ( y ` ( F ` c ) ) e. B )
138 136 131 137 syl2an 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( y ` ( F ` c ) ) e. B )
139 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 ) ) ) ) )
140 125 133 138 139 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 ) ) ) ) )
141 fvex 
 |-  ( `' G ` ( y ` ( F ` c ) ) ) e. _V
142 141 epeli 
 |-  ( ( `' G ` ( x ` ( F ` c ) ) ) _E ( `' G ` ( y ` ( F ` c ) ) ) <-> ( `' G ` ( x ` ( F ` c ) ) ) e. ( `' G ` ( y ` ( F ` c ) ) ) )
143 140 142 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 ) ) ) ) )
144 129 adantr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> x : A --> B )
145 fco 
 |-  ( ( x : A --> B /\ F : dom F --> A ) -> ( x o. F ) : dom F --> B )
146 144 130 145 sylancl 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( x o. F ) : dom F --> B )
147 fvco3 
 |-  ( ( ( x o. F ) : dom F --> B /\ c e. dom F ) -> ( ( `' G o. ( x o. F ) ) ` c ) = ( `' G ` ( ( x o. F ) ` c ) ) )
148 146 147 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 ) ) )
149 simpr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> c e. dom F )
150 fvco3 
 |-  ( ( F : dom F --> A /\ c e. dom F ) -> ( ( x o. F ) ` c ) = ( x ` ( F ` c ) ) )
151 130 149 150 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 ) ) )
152 151 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 ) ) ) )
153 148 152 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 ) ) ) )
154 136 adantr 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> y : A --> B )
155 fco 
 |-  ( ( y : A --> B /\ F : dom F --> A ) -> ( y o. F ) : dom F --> B )
156 154 130 155 sylancl 
 |-  ( ( ( ( ph /\ ( B e. _V /\ A e. _V ) ) /\ ( x e. U /\ y e. U ) ) /\ c e. dom F ) -> ( y o. F ) : dom F --> B )
157 fvco3 
 |-  ( ( ( y o. F ) : dom F --> B /\ c e. dom F ) -> ( ( `' G o. ( y o. F ) ) ` c ) = ( `' G ` ( ( y o. F ) ` c ) ) )
158 156 157 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 ) ) )
159 fvco3 
 |-  ( ( F : dom F --> A /\ c e. dom F ) -> ( ( y o. F ) ` c ) = ( y ` ( F ` c ) ) )
160 130 149 159 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 ) ) )
161 160 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 ) ) ) )
162 158 161 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 ) ) ) )
163 153 162 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 ) ) ) ) )
164 143 163 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 ) ) )
165 86 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 ) ) ) )
166 breq2 
 |-  ( w = ( F ` d ) -> ( ( F ` c ) R w <-> ( F ` c ) R ( F ` d ) ) )
167 fveq2 
 |-  ( w = ( F ` d ) -> ( x ` w ) = ( x ` ( F ` d ) ) )
168 fveq2 
 |-  ( w = ( F ` d ) -> ( y ` w ) = ( y ` ( F ` d ) ) )
169 167 168 eqeq12d 
 |-  ( w = ( F ` d ) -> ( ( x ` w ) = ( y ` w ) <-> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) )
170 166 169 imbi12d 
 |-  ( w = ( F ` d ) -> ( ( ( F ` c ) R w -> ( x ` w ) = ( y ` w ) ) <-> ( ( F ` c ) R ( F ` d ) -> ( x ` ( F ` d ) ) = ( y ` ( F ` d ) ) ) ) )
171 170 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 ) ) ) ) )
172 73 74 171 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 ) ) ) ) )
173 165 172 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 ) ) ) ) )
174 173 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 ) ) ) ) )
175 epel 
 |-  ( c _E d <-> c e. d )
176 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 ) )
177 isorel 
 |-  ( ( F Isom _E , R ( dom F , A ) /\ ( c e. dom F /\ d e. dom F ) ) -> ( c _E d <-> ( F ` c ) R ( F ` d ) ) )
178 176 177 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 ) ) )
179 175 178 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 ) ) )
180 146 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 )
181 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 )
182 180 181 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 ) ) )
183 156 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 )
184 183 181 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 ) ) )
185 182 184 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 ) ) ) )
186 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 )
187 f1of1 
 |-  ( `' G : B -1-1-onto-> dom G -> `' G : B -1-1-> dom G )
188 186 22 187 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 )
189 180 181 ffvelcdmd 
 |-  ( ( ( ( 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 )
190 183 181 ffvelcdmd 
 |-  ( ( ( ( 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 )
191 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 ) ) )
192 188 189 190 191 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 ) ) )
193 fvco3 
 |-  ( ( F : dom F --> A /\ d e. dom F ) -> ( ( x o. F ) ` d ) = ( x ` ( F ` d ) ) )
194 130 181 193 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 ) ) )
195 fvco3 
 |-  ( ( F : dom F --> A /\ d e. dom F ) -> ( ( y o. F ) ` d ) = ( y ` ( F ` d ) ) )
196 130 181 195 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 ) ) )
197 194 196 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 ) ) ) )
198 185 192 197 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 ) ) ) )
199 179 198 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 ) ) ) ) )
200 199 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 ) ) ) ) )
201 200 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 ) ) ) ) )
202 174 201 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 ) ) ) )
203 164 202 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 ) ) ) ) )
204 203 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 ) ) ) ) )
205 112 122 204 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 ) ) )
206 83 87 205 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 ) ) )
207 206 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 ) ) ) )
208 207 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 ) ) ) )
209 208 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 ) ) } )
210 df-xp 
 |-  ( U X. U ) = { <. x , y >. | ( x e. U /\ y e. U ) }
211 1 210 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 ) } )
212 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 ) ) }
213 211 212 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 ) ) }
214 210 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 ) } )
215 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 ) ) }
216 214 215 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 ) ) }
217 209 213 216 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 ) ) )
218 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 ) )
219 217 218 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 ) )
220 72 219 mpbird 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> ( T i^i ( U X. U ) ) We U )
221 weinxp 
 |-  ( T We U <-> ( T i^i ( U X. U ) ) We U )
222 220 221 sylibr 
 |-  ( ( ph /\ ( B e. _V /\ A e. _V ) ) -> T We U )
223 222 ex 
 |-  ( ph -> ( ( B e. _V /\ A e. _V ) -> T We U ) )
224 we0 
 |-  T We (/)
225 elmapex 
 |-  ( x e. ( B ^m A ) -> ( B e. _V /\ A e. _V ) )
226 225 con3i 
 |-  ( -. ( B e. _V /\ A e. _V ) -> -. x e. ( B ^m A ) )
227 226 pm2.21d 
 |-  ( -. ( B e. _V /\ A e. _V ) -> ( x e. ( B ^m A ) -> -. x finSupp Z ) )
228 227 ralrimiv 
 |-  ( -. ( B e. _V /\ A e. _V ) -> A. x e. ( B ^m A ) -. x finSupp Z )
229 rabeq0 
 |-  ( { x e. ( B ^m A ) | x finSupp Z } = (/) <-> A. x e. ( B ^m A ) -. x finSupp Z )
230 228 229 sylibr 
 |-  ( -. ( B e. _V /\ A e. _V ) -> { x e. ( B ^m A ) | x finSupp Z } = (/) )
231 2 230 eqtrid 
 |-  ( -. ( B e. _V /\ A e. _V ) -> U = (/) )
232 weeq2 
 |-  ( U = (/) -> ( T We U <-> T We (/) ) )
233 231 232 syl 
 |-  ( -. ( B e. _V /\ A e. _V ) -> ( T We U <-> T We (/) ) )
234 224 233 mpbiri 
 |-  ( -. ( B e. _V /\ A e. _V ) -> T We U )
235 223 234 pm2.61d1 
 |-  ( ph -> T We U )