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 \land R Se A \land F {Isom}_{R, R} (A, A)) \to F = {I ↾}_{A}$

Proof

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

Metamath Proof Explorer

Theorem weniso

Proof