Metamath Proof Explorer

Theorem weniso

Description: A set-like well-ordering has no nontrivial automorphisms. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion weniso 
|- ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> F = ( _I |` A ) )

Proof

Step Hyp Ref Expression
1 rabn0 
 |-  ( { a e. A | -. ( F ` a ) = a } =/= (/) <-> E. a e. A -. ( F ` a ) = a )
2 rexnal 
 |-  ( E. a e. A -. ( F ` a ) = a <-> -. A. a e. A ( F ` a ) = a )
3 1 2 bitri 
 |-  ( { a e. A | -. ( F ` a ) = a } =/= (/) <-> -. A. a e. A ( F ` a ) = a )
4 simpl1 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ { a e. A | -. ( F ` a ) = a } =/= (/) ) -> R We A )
5 simpl2 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ { a e. A | -. ( F ` a ) = a } =/= (/) ) -> R Se A )
6 ssrab2 
 |-  { a e. A | -. ( F ` a ) = a } C_ A
7 6 a1i 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ { a e. A | -. ( F ` a ) = a } =/= (/) ) -> { a e. A | -. ( F ` a ) = a } C_ A )
8 simpr 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ { a e. A | -. ( F ` a ) = a } =/= (/) ) -> { a e. A | -. ( F ` a ) = a } =/= (/) )
9 wereu2 
 |-  ( ( ( R We A /\ R Se A ) /\ ( { a e. A | -. ( F ` a ) = a } C_ A /\ { a e. A | -. ( F ` a ) = a } =/= (/) ) ) -> E! b e. { a e. A | -. ( F ` a ) = a } A. c e. { a e. A | -. ( F ` a ) = a } -. c R b )
10 4 5 7 8 9 syl22anc 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ { a e. A | -. ( F ` a ) = a } =/= (/) ) -> E! b e. { a e. A | -. ( F ` a ) = a } A. c e. { a e. A | -. ( F ` a ) = a } -. c R b )
11 reurex 
 |-  ( E! b e. { a e. A | -. ( F ` a ) = a } A. c e. { a e. A | -. ( F ` a ) = a } -. c R b -> E. b e. { a e. A | -. ( F ` a ) = a } A. c e. { a e. A | -. ( F ` a ) = a } -. c R b )
12 10 11 syl 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ { a e. A | -. ( F ` a ) = a } =/= (/) ) -> E. b e. { a e. A | -. ( F ` a ) = a } A. c e. { a e. A | -. ( F ` a ) = a } -. c R b )
13 12 ex 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> ( { a e. A | -. ( F ` a ) = a } =/= (/) -> E. b e. { a e. A | -. ( F ` a ) = a } A. c e. { a e. A | -. ( F ` a ) = a } -. c R b ) )
14 fveq2 
 |-  ( a = b -> ( F ` a ) = ( F ` b ) )
15 id 
 |-  ( a = b -> a = b )
16 14 15 eqeq12d 
 |-  ( a = b -> ( ( F ` a ) = a <-> ( F ` b ) = b ) )
17 16 notbid 
 |-  ( a = b -> ( -. ( F ` a ) = a <-> -. ( F ` b ) = b ) )
18 17 elrab 
 |-  ( b e. { a e. A | -. ( F ` a ) = a } <-> ( b e. A /\ -. ( F ` b ) = b ) )
19 fveq2 
 |-  ( a = c -> ( F ` a ) = ( F ` c ) )
20 id 
 |-  ( a = c -> a = c )
21 19 20 eqeq12d 
 |-  ( a = c -> ( ( F ` a ) = a <-> ( F ` c ) = c ) )
22 21 notbid 
 |-  ( a = c -> ( -. ( F ` a ) = a <-> -. ( F ` c ) = c ) )
23 22 ralrab 
 |-  ( A. c e. { a e. A | -. ( F ` a ) = a } -. c R b <-> A. c e. A ( -. ( F ` c ) = c -> -. c R b ) )
24 con34b 
 |-  ( ( c R b -> ( F ` c ) = c ) <-> ( -. ( F ` c ) = c -> -. c R b ) )
25 24 bicomi 
 |-  ( ( -. ( F ` c ) = c -> -. c R b ) <-> ( c R b -> ( F ` c ) = c ) )
26 25 ralbii 
 |-  ( A. c e. A ( -. ( F ` c ) = c -> -. c R b ) <-> A. c e. A ( c R b -> ( F ` c ) = c ) )
27 23 26 bitri 
 |-  ( A. c e. { a e. A | -. ( F ` a ) = a } -. c R b <-> A. c e. A ( c R b -> ( F ` c ) = c ) )
28 simpl3 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> F Isom R , R ( A , A ) )
29 isof1o 
 |-  ( F Isom R , R ( A , A ) -> F : A -1-1-onto-> A )
30 28 29 syl 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> F : A -1-1-onto-> A )
31 f1of 
 |-  ( F : A -1-1-onto-> A -> F : A --> A )
32 30 31 syl 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> F : A --> A )
33 simprl 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> b e. A )
34 32 33 ffvelcdmd 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( F ` b ) e. A )
35 breq1 
 |-  ( c = ( F ` b ) -> ( c R b <-> ( F ` b ) R b ) )
36 fveq2 
 |-  ( c = ( F ` b ) -> ( F ` c ) = ( F ` ( F ` b ) ) )
37 id 
 |-  ( c = ( F ` b ) -> c = ( F ` b ) )
38 36 37 eqeq12d 
 |-  ( c = ( F ` b ) -> ( ( F ` c ) = c <-> ( F ` ( F ` b ) ) = ( F ` b ) ) )
39 35 38 imbi12d 
 |-  ( c = ( F ` b ) -> ( ( c R b -> ( F ` c ) = c ) <-> ( ( F ` b ) R b -> ( F ` ( F ` b ) ) = ( F ` b ) ) ) )
40 39 rspcv 
 |-  ( ( F ` b ) e. A -> ( A. c e. A ( c R b -> ( F ` c ) = c ) -> ( ( F ` b ) R b -> ( F ` ( F ` b ) ) = ( F ` b ) ) ) )
41 34 40 syl 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( A. c e. A ( c R b -> ( F ` c ) = c ) -> ( ( F ` b ) R b -> ( F ` ( F ` b ) ) = ( F ` b ) ) ) )
42 41 com23 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( ( F ` b ) R b -> ( A. c e. A ( c R b -> ( F ` c ) = c ) -> ( F ` ( F ` b ) ) = ( F ` b ) ) ) )
43 42 imp 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ ( F ` b ) R b ) -> ( A. c e. A ( c R b -> ( F ` c ) = c ) -> ( F ` ( F ` b ) ) = ( F ` b ) ) )
44 f1of1 
 |-  ( F : A -1-1-onto-> A -> F : A -1-1-> A )
45 30 44 syl 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> F : A -1-1-> A )
46 f1fveq 
 |-  ( ( F : A -1-1-> A /\ ( ( F ` b ) e. A /\ b e. A ) ) -> ( ( F ` ( F ` b ) ) = ( F ` b ) <-> ( F ` b ) = b ) )
47 45 34 33 46 syl12anc 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( ( F ` ( F ` b ) ) = ( F ` b ) <-> ( F ` b ) = b ) )
48 pm2.21 
 |-  ( -. ( F ` b ) = b -> ( ( F ` b ) = b -> A. a e. A ( F ` a ) = a ) )
49 48 ad2antll 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( ( F ` b ) = b -> A. a e. A ( F ` a ) = a ) )
50 47 49 sylbid 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( ( F ` ( F ` b ) ) = ( F ` b ) -> A. a e. A ( F ` a ) = a ) )
51 50 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ ( F ` b ) R b ) -> ( ( F ` ( F ` b ) ) = ( F ` b ) -> A. a e. A ( F ` a ) = a ) )
52 43 51 syld 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ ( F ` b ) R b ) -> ( A. c e. A ( c R b -> ( F ` c ) = c ) -> A. a e. A ( F ` a ) = a ) )
53 f1ocnv 
 |-  ( F : A -1-1-onto-> A -> `' F : A -1-1-onto-> A )
54 f1of 
 |-  ( `' F : A -1-1-onto-> A -> `' F : A --> A )
55 30 53 54 3syl 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> `' F : A --> A )
56 55 33 ffvelcdmd 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( `' F ` b ) e. A )
57 56 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ b R ( F ` b ) ) -> ( `' F ` b ) e. A )
58 isorel 
 |-  ( ( F Isom R , R ( A , A ) /\ ( ( `' F ` b ) e. A /\ b e. A ) ) -> ( ( `' F ` b ) R b <-> ( F ` ( `' F ` b ) ) R ( F ` b ) ) )
59 28 56 33 58 syl12anc 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( ( `' F ` b ) R b <-> ( F ` ( `' F ` b ) ) R ( F ` b ) ) )
60 f1ocnvfv2 
 |-  ( ( F : A -1-1-onto-> A /\ b e. A ) -> ( F ` ( `' F ` b ) ) = b )
61 30 33 60 syl2anc 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( F ` ( `' F ` b ) ) = b )
62 61 breq1d 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( ( F ` ( `' F ` b ) ) R ( F ` b ) <-> b R ( F ` b ) ) )
63 59 62 bitr2d 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( b R ( F ` b ) <-> ( `' F ` b ) R b ) )
64 63 biimpa 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ b R ( F ` b ) ) -> ( `' F ` b ) R b )
65 breq1 
 |-  ( c = ( `' F ` b ) -> ( c R b <-> ( `' F ` b ) R b ) )
66 fveq2 
 |-  ( c = ( `' F ` b ) -> ( F ` c ) = ( F ` ( `' F ` b ) ) )
67 id 
 |-  ( c = ( `' F ` b ) -> c = ( `' F ` b ) )
68 66 67 eqeq12d 
 |-  ( c = ( `' F ` b ) -> ( ( F ` c ) = c <-> ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) )
69 65 68 imbi12d 
 |-  ( c = ( `' F ` b ) -> ( ( c R b -> ( F ` c ) = c ) <-> ( ( `' F ` b ) R b -> ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) ) )
70 69 rspcv 
 |-  ( ( `' F ` b ) e. A -> ( A. c e. A ( c R b -> ( F ` c ) = c ) -> ( ( `' F ` b ) R b -> ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) ) )
71 70 com23 
 |-  ( ( `' F ` b ) e. A -> ( ( `' F ` b ) R b -> ( A. c e. A ( c R b -> ( F ` c ) = c ) -> ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) ) )
72 57 64 71 sylc 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ b R ( F ` b ) ) -> ( A. c e. A ( c R b -> ( F ` c ) = c ) -> ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) )
73 simplrr 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) -> -. ( F ` b ) = b )
74 fveq2 
 |-  ( ( F ` ( `' F ` b ) ) = ( `' F ` b ) -> ( F ` ( F ` ( `' F ` b ) ) ) = ( F ` ( `' F ` b ) ) )
75 74 adantl 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) -> ( F ` ( F ` ( `' F ` b ) ) ) = ( F ` ( `' F ` b ) ) )
76 61 fveq2d 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( F ` ( F ` ( `' F ` b ) ) ) = ( F ` b ) )
77 76 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) -> ( F ` ( F ` ( `' F ` b ) ) ) = ( F ` b ) )
78 61 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) -> ( F ` ( `' F ` b ) ) = b )
79 75 77 78 3eqtr3d 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) -> ( F ` b ) = b )
80 73 79 48 sylc 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) -> A. a e. A ( F ` a ) = a )
81 80 ex 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( ( F ` ( `' F ` b ) ) = ( `' F ` b ) -> A. a e. A ( F ` a ) = a ) )
82 81 adantr 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ b R ( F ` b ) ) -> ( ( F ` ( `' F ` b ) ) = ( `' F ` b ) -> A. a e. A ( F ` a ) = a ) )
83 72 82 syld 
 |-  ( ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) /\ b R ( F ` b ) ) -> ( A. c e. A ( c R b -> ( F ` c ) = c ) -> A. a e. A ( F ` a ) = a ) )
84 simprr 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> -. ( F ` b ) = b )
85 simpl1 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> R We A )
86 weso 
 |-  ( R We A -> R Or A )
87 85 86 syl 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> R Or A )
88 sotrieq 
 |-  ( ( R Or A /\ ( ( F ` b ) e. A /\ b e. A ) ) -> ( ( F ` b ) = b <-> -. ( ( F ` b ) R b \/ b R ( F ` b ) ) ) )
89 87 34 33 88 syl12anc 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( ( F ` b ) = b <-> -. ( ( F ` b ) R b \/ b R ( F ` b ) ) ) )
90 89 con2bid 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( ( ( F ` b ) R b \/ b R ( F ` b ) ) <-> -. ( F ` b ) = b ) )
91 84 90 mpbird 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( ( F ` b ) R b \/ b R ( F ` b ) ) )
92 52 83 91 mpjaodan 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( A. c e. A ( c R b -> ( F ` c ) = c ) -> A. a e. A ( F ` a ) = a ) )
93 27 92 biimtrid 
 |-  ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( A. c e. { a e. A | -. ( F ` a ) = a } -. c R b -> A. a e. A ( F ` a ) = a ) )
94 93 ex 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> ( ( b e. A /\ -. ( F ` b ) = b ) -> ( A. c e. { a e. A | -. ( F ` a ) = a } -. c R b -> A. a e. A ( F ` a ) = a ) ) )
95 18 94 biimtrid 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> ( b e. { a e. A | -. ( F ` a ) = a } -> ( A. c e. { a e. A | -. ( F ` a ) = a } -. c R b -> A. a e. A ( F ` a ) = a ) ) )
96 95 rexlimdv 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> ( E. b e. { a e. A | -. ( F ` a ) = a } A. c e. { a e. A | -. ( F ` a ) = a } -. c R b -> A. a e. A ( F ` a ) = a ) )
97 13 96 syld 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> ( { a e. A | -. ( F ` a ) = a } =/= (/) -> A. a e. A ( F ` a ) = a ) )
98 3 97 biimtrrid 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> ( -. A. a e. A ( F ` a ) = a -> A. a e. A ( F ` a ) = a ) )
99 98 pm2.18d 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> A. a e. A ( F ` a ) = a )
100 fvresi 
 |-  ( a e. A -> ( ( _I |` A ) ` a ) = a )
101 100 eqeq2d 
 |-  ( a e. A -> ( ( F ` a ) = ( ( _I |` A ) ` a ) <-> ( F ` a ) = a ) )
102 101 biimprd 
 |-  ( a e. A -> ( ( F ` a ) = a -> ( F ` a ) = ( ( _I |` A ) ` a ) ) )
103 102 ralimia 
 |-  ( A. a e. A ( F ` a ) = a -> A. a e. A ( F ` a ) = ( ( _I |` A ) ` a ) )
104 99 103 syl 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> A. a e. A ( F ` a ) = ( ( _I |` A ) ` a ) )
105 29 3ad2ant3 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> F : A -1-1-onto-> A )
106 f1ofn 
 |-  ( F : A -1-1-onto-> A -> F Fn A )
107 105 106 syl 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> F Fn A )
108 fnresi 
 |-  ( _I |` A ) Fn A
109 108 a1i 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> ( _I |` A ) Fn A )
110 eqfnfv 
 |-  ( ( F Fn A /\ ( _I |` A ) Fn A ) -> ( F = ( _I |` A ) <-> A. a e. A ( F ` a ) = ( ( _I |` A ) ` a ) ) )
111 107 109 110 syl2anc 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> ( F = ( _I |` A ) <-> A. a e. A ( F ` a ) = ( ( _I |` A ) ` a ) ) )
112 104 111 mpbird 
 |-  ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> F = ( _I |` A ) )