Theorem weniso 6604

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.)

Assertion

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

Proof of Theorem weniso

Dummy variables a b c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabn0 3958	. . . . . 6 |- ( { a e. A | -. ( F ` a ) = a } =/= (/) <-> E. a e. A -. ( F ` a ) = a )
2		rexnal 2995	. . . . . 6 |- ( E. a e. A -. ( F ` a ) = a <-> -. A. a e. A ( F ` a ) = a )
3	1, 2	bitri 264	. . . . 5 |- ( { a e. A | -. ( F ` a ) = a } =/= (/) <-> -. A. a e. A ( F ` a ) = a )
4		simpl1 1064	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ { a e. A | -. ( F ` a ) = a } =/= (/) ) -> R We A )
5		simpl2 1065	. . . . . . . . 9 |- ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ { a e. A | -. ( F ` a ) = a } =/= (/) ) -> R Se A )
6		ssrab2 3687	. . . . . . . . . 10 |- { a e. A | -. ( F ` a ) = a } C_ A
7	6	a1i 11	. . . . . . . . 9 |- ( ( ( 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 477	. . . . . . . . 9 |- ( ( ( 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 5111	. . . . . . . . 9 |- ( ( ( 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 1327	. . . . . . . 8 |- ( ( ( 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 3160	. . . . . . . 8 |- ( 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 17	. . . . . . 7 |- ( ( ( 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 450	. . . . . 6 |- ( ( 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 6191	. . . . . . . . . . 11 |- ( a = b -> ( F ` a ) = ( F ` b ) )
15		id 22	. . . . . . . . . . 11 |- ( a = b -> a = b )
16	14, 15	eqeq12d 2637	. . . . . . . . . 10 |- ( a = b -> ( ( F ` a ) = a <-> ( F ` b ) = b ) )
17	16	notbid 308	. . . . . . . . 9 |- ( a = b -> ( -. ( F ` a ) = a <-> -. ( F ` b ) = b ) )
18	17	elrab 3363	. . . . . . . 8 |- ( b e. { a e. A | -. ( F ` a ) = a } <-> ( b e. A /\ -. ( F ` b ) = b ) )
19		fveq2 6191	. . . . . . . . . . . . . 14 |- ( a = c -> ( F ` a ) = ( F ` c ) )
20		id 22	. . . . . . . . . . . . . 14 |- ( a = c -> a = c )
21	19, 20	eqeq12d 2637	. . . . . . . . . . . . 13 |- ( a = c -> ( ( F ` a ) = a <-> ( F ` c ) = c ) )
22	21	notbid 308	. . . . . . . . . . . 12 |- ( a = c -> ( -. ( F ` a ) = a <-> -. ( F ` c ) = c ) )
23	22	ralrab 3368	. . . . . . . . . . 11 |- ( A. c e. { a e. A | -. ( F ` a ) = a } -. c R b <-> A. c e. A ( -. ( F ` c ) = c -> -. c R b ) )
24		con34b 306	. . . . . . . . . . . . 13 |- ( ( c R b -> ( F ` c ) = c ) <-> ( -. ( F ` c ) = c -> -. c R b ) )
25	24	bicomi 214	. . . . . . . . . . . 12 |- ( ( -. ( F ` c ) = c -> -. c R b ) <-> ( c R b -> ( F ` c ) = c ) )
26	25	ralbii 2980	. . . . . . . . . . 11 |- ( A. c e. A ( -. ( F ` c ) = c -> -. c R b ) <-> A. c e. A ( c R b -> ( F ` c ) = c ) )
27	23, 26	bitri 264	. . . . . . . . . 10 |- ( A. c e. { a e. A | -. ( F ` a ) = a } -. c R b <-> A. c e. A ( c R b -> ( F ` c ) = c ) )
28		simpl3 1066	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 6573	. . . . . . . . . . . . . . . . . 18 |- ( F Isom R , R ( A , A ) -> F : A -1-1-onto-> A )
30	28, 29	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 6137	. . . . . . . . . . . . . . . . 17 |- ( F : A -1-1-onto-> A -> F : A --> A )
32	30, 31	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> F : A --> A )
33		simprl 794	. . . . . . . . . . . . . . . 16 |- ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> b e. A )
34	32, 33	ffvelrnd 6360	. . . . . . . . . . . . . . 15 |- ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> ( F ` b ) e. A )
35		breq1 4656	. . . . . . . . . . . . . . . . 17 |- ( c = ( F ` b ) -> ( c R b <-> ( F ` b ) R b ) )
36		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( c = ( F ` b ) -> ( F ` c ) = ( F ` ( F ` b ) ) )
37		id 22	. . . . . . . . . . . . . . . . . 18 |- ( c = ( F ` b ) -> c = ( F ` b ) )
38	36, 37	eqeq12d 2637	. . . . . . . . . . . . . . . . 17 |- ( c = ( F ` b ) -> ( ( F ` c ) = c <-> ( F ` ( F ` b ) ) = ( F ` b ) ) )
39	35, 38	imbi12d 334	. . . . . . . . . . . . . . . 16 |- ( c = ( F ` b ) -> ( ( c R b -> ( F ` c ) = c ) <-> ( ( F ` b ) R b -> ( F ` ( F ` b ) ) = ( F ` b ) ) ) )
40	39	rspcv 3305	. . . . . . . . . . . . . . 15 |- ( ( 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 17	. . . . . . . . . . . . . 14 |- ( ( ( 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 86	. . . . . . . . . . . . 13 |- ( ( ( 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 445	. . . . . . . . . . . 12 |- ( ( ( ( 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 6136	. . . . . . . . . . . . . . . 16 |- ( F : A -1-1-onto-> A -> F : A -1-1-> A )
45	30, 44	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( 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 6519	. . . . . . . . . . . . . . 15 |- ( ( 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 1324	. . . . . . . . . . . . . 14 |- ( ( ( 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 120	. . . . . . . . . . . . . . 15 |- ( -. ( F ` b ) = b -> ( ( F ` b ) = b -> A. a e. A ( F ` a ) = a ) )
49	48	ad2antll 765	. . . . . . . . . . . . . 14 |- ( ( ( 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 230	. . . . . . . . . . . . 13 |- ( ( ( 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 481	. . . . . . . . . . . 12 |- ( ( ( ( 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 47	. . . . . . . . . . 11 |- ( ( ( ( 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 6149	. . . . . . . . . . . . . . . 16 |- ( F : A -1-1-onto-> A -> `' F : A -1-1-onto-> A )
54		f1of 6137	. . . . . . . . . . . . . . . 16 |- ( `' F : A -1-1-onto-> A -> `' F : A --> A )
55	30, 53, 54	3syl 18	. . . . . . . . . . . . . . 15 |- ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> `' F : A --> A )
56	55, 33	ffvelrnd 6360	. . . . . . . . . . . . . 14 |- ( ( ( 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 481	. . . . . . . . . . . . 13 |- ( ( ( ( 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 6576	. . . . . . . . . . . . . . . 16 |- ( ( 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 1324	. . . . . . . . . . . . . . 15 |- ( ( ( 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 6533	. . . . . . . . . . . . . . . . 17 |- ( ( F : A -1-1-onto-> A /\ b e. A ) -> ( F ` ( `' F ` b ) ) = b )
61	30, 33, 60	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 4663	. . . . . . . . . . . . . . 15 |- ( ( ( 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 269	. . . . . . . . . . . . . 14 |- ( ( ( 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 501	. . . . . . . . . . . . 13 |- ( ( ( ( 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 4656	. . . . . . . . . . . . . . . 16 |- ( c = ( `' F ` b ) -> ( c R b <-> ( `' F ` b ) R b ) )
66		fveq2 6191	. . . . . . . . . . . . . . . . 17 |- ( c = ( `' F ` b ) -> ( F ` c ) = ( F ` ( `' F ` b ) ) )
67		id 22	. . . . . . . . . . . . . . . . 17 |- ( c = ( `' F ` b ) -> c = ( `' F ` b ) )
68	66, 67	eqeq12d 2637	. . . . . . . . . . . . . . . 16 |- ( c = ( `' F ` b ) -> ( ( F ` c ) = c <-> ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) )
69	65, 68	imbi12d 334	. . . . . . . . . . . . . . 15 |- ( c = ( `' F ` b ) -> ( ( c R b -> ( F ` c ) = c ) <-> ( ( `' F ` b ) R b -> ( F ` ( `' F ` b ) ) = ( `' F ` b ) ) ) )
70	69	rspcv 3305	. . . . . . . . . . . . . 14 |- ( ( `' 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 86	. . . . . . . . . . . . 13 |- ( ( `' 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 65	. . . . . . . . . . . 12 |- ( ( ( ( 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 801	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 6191	. . . . . . . . . . . . . . . . 17 |- ( ( F ` ( `' F ` b ) ) = ( `' F ` b ) -> ( F ` ( F ` ( `' F ` b ) ) ) = ( F ` ( `' F ` b ) ) )
75	74	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 6195	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 2664	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 65	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 450	. . . . . . . . . . . . 13 |- ( ( ( 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 481	. . . . . . . . . . . 12 |- ( ( ( ( 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 47	. . . . . . . . . . 11 |- ( ( ( ( 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 796	. . . . . . . . . . . 12 |- ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> -. ( F ` b ) = b )
85		simpl1 1064	. . . . . . . . . . . . . . 15 |- ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> R We A )
86		weso 5105	. . . . . . . . . . . . . . 15 |- ( R We A -> R Or A )
87	85, 86	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) /\ ( b e. A /\ -. ( F ` b ) = b ) ) -> R Or A )
88		sotrieq 5062	. . . . . . . . . . . . . 14 |- ( ( 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 1324	. . . . . . . . . . . . 13 |- ( ( ( 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 344	. . . . . . . . . . . 12 |- ( ( ( 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 247	. . . . . . . . . . 11 |- ( ( ( 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 827	. . . . . . . . . 10 |- ( ( ( 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	syl5bi 232	. . . . . . . . 9 |- ( ( ( 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 450	. . . . . . . 8 |- ( ( 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	syl5bi 232	. . . . . . 7 |- ( ( 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 3030	. . . . . 6 |- ( ( 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 47	. . . . 5 |- ( ( 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	syl5bir 233	. . . 4 |- ( ( 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 124	. . 3 |- ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> A. a e. A ( F ` a ) = a )
100		fvresi 6439	. . . . . 6 |- ( a e. A -> ( ( _I |` A ) ` a ) = a )
101	100	eqeq2d 2632	. . . . 5 |- ( a e. A -> ( ( F ` a ) = ( ( _I |` A ) ` a ) <-> ( F ` a ) = a ) )
102	101	biimprd 238	. . . 4 |- ( a e. A -> ( ( F ` a ) = a -> ( F ` a ) = ( ( _I |` A ) ` a ) ) )
103	102	ralimia 2950	. . 3 |- ( A. a e. A ( F ` a ) = a -> A. a e. A ( F ` a ) = ( ( _I |` A ) ` a ) )
104	99, 103	syl 17	. 2 |- ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> A. a e. A ( F ` a ) = ( ( _I |` A ) ` a ) )
105	29	3ad2ant3 1084	. . . 4 |- ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> F : A -1-1-onto-> A )
106		f1ofn 6138	. . . 4 |- ( F : A -1-1-onto-> A -> F Fn A )
107	105, 106	syl 17	. . 3 |- ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> F Fn A )
108		fnresi 6008	. . . 4 |- ( _I |` A ) Fn A
109	108	a1i 11	. . 3 |- ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> ( _I |` A ) Fn A )
110		eqfnfv 6311	. . 3 |- ( ( F Fn A /\ ( _I |` A ) Fn A ) -> ( F = ( _I |` A ) <-> A. a e. A ( F ` a ) = ( ( _I |` A ) ` a ) ) )
111	107, 109, 110	syl2anc 693	. 2 |- ( ( 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 247	1 |- ( ( R We A /\ R Se A /\ F Isom R , R ( A , A ) ) -> F = ( _I |` A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   E!wreu 2914   {crab 2916   C_ wss 3574   (/)c0 3915   class class class wbr 4653   _I cid 5023   Or wor 5034   Se wse 5071   We wwe 5072   `'ccnv 5113   |` cres 5116   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -1-1-onto->wf1o 5887   ` cfv 5888   Isom wiso 5889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897

This theorem is referenced by:  weisoeq  6605  oiid  8446