Theorem weniso 7295

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	⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴))

Proof of Theorem weniso

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabn0 4343	. . . . . 6 ⊢ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ ↔ ∃𝑎 ∈ 𝐴 ¬ (𝐹‘𝑎) = 𝑎)
2		rexnal 3101	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 ¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
3	1, 2	bitri 274	. . . . 5 ⊢ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ ↔ ¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
4		simpl1 1191	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → 𝑅 We 𝐴)
5		simpl2 1192	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → 𝑅 Se 𝐴)
6		ssrab2 4035	. . . . . . . . . 10 ⊢ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴
7	6	a1i 11	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴)
8		simpr 485	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅)
9		wereu2 5628	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴 ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅)) → ∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
10	4, 5, 7, 8, 9	syl22anc 837	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → ∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
11		reurex 3355	. . . . . . . 8 ⊢ (∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
12	10, 11	syl 17	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
13	12	ex 413	. . . . . 6 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏))
14		fveq2 6839	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏))
15		id 22	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏)
16	14, 15	eqeq12d 2753	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → ((𝐹‘𝑎) = 𝑎 ↔ (𝐹‘𝑏) = 𝑏))
17	16	notbid 317	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ (𝐹‘𝑏) = 𝑏))
18	17	elrab 3643	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ↔ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏))
19		fveq2 6839	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
20		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
21	19, 20	eqeq12d 2753	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) = 𝑎 ↔ (𝐹‘𝑐) = 𝑐))
22	21	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ (𝐹‘𝑐) = 𝑐))
23	22	ralrab 3649	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ 𝐴 (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
24		con34b 315	. . . . . . . . . . . . 13 ⊢ ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
25	24	bicomi 223	. . . . . . . . . . . 12 ⊢ ((¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
26	25	ralbii 3094	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ 𝐴 (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
27	23, 26	bitri 274	. . . . . . . . . 10 ⊢ (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
28		simpl3 1193	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴))
29		isof1o 7264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) → 𝐹:𝐴–1-1-onto→𝐴)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴–1-1-onto→𝐴)
31		f1of 6781	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴⟶𝐴)
32	30, 31	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴⟶𝐴)
33		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑏 ∈ 𝐴)
34	32, 33	ffvelcdmd 7032	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘𝑏) ∈ 𝐴)
35		breq1 5106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑏) → (𝑐𝑅𝑏 ↔ (𝐹‘𝑏)𝑅𝑏))
36		fveq2 6839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑏) → (𝐹‘𝑐) = (𝐹‘(𝐹‘𝑏)))
37		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑏) → 𝑐 = (𝐹‘𝑏))
38	36, 37	eqeq12d 2753	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑏) → ((𝐹‘𝑐) = 𝑐 ↔ (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏)))
39	35, 38	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑏) → ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
40	39	rspcv 3575	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑏) ∈ 𝐴 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
41	34, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
42	41	com23 86	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏)𝑅𝑏 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
43	42	imp 407	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏)))
44		f1of1 6780	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴–1-1→𝐴)
45	30, 44	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴–1-1→𝐴)
46		f1fveq 7205	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴–1-1→𝐴 ∧ ((𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) ↔ (𝐹‘𝑏) = 𝑏))
47	45, 34, 33, 46	syl12anc 835	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) ↔ (𝐹‘𝑏) = 𝑏))
48		pm2.21 123	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝐹‘𝑏) = 𝑏 → ((𝐹‘𝑏) = 𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
49	48	ad2antll 727	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏) = 𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
50	47, 49	sylbid 239	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
51	50	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
52	43, 51	syld 47	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
53		f1ocnv 6793	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐴)
54		f1of 6781	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹:𝐴–1-1-onto→𝐴 → ◡𝐹:𝐴⟶𝐴)
55	30, 53, 54	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ◡𝐹:𝐴⟶𝐴)
56	55, 33	ffvelcdmd 7032	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (◡𝐹‘𝑏) ∈ 𝐴)
57	56	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (◡𝐹‘𝑏) ∈ 𝐴)
58		isorel 7267	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) ∧ ((◡𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((◡𝐹‘𝑏)𝑅𝑏 ↔ (𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏)))
59	28, 56, 33, 58	syl12anc 835	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((◡𝐹‘𝑏)𝑅𝑏 ↔ (𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏)))
60		f1ocnvfv2 7219	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
61	30, 33, 60	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
62	61	breq1d 5113	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏) ↔ 𝑏𝑅(𝐹‘𝑏)))
63	59, 62	bitr2d 279	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝑏𝑅(𝐹‘𝑏) ↔ (◡𝐹‘𝑏)𝑅𝑏))
64	63	biimpa 477	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (◡𝐹‘𝑏)𝑅𝑏)
65		breq1 5106	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (◡𝐹‘𝑏) → (𝑐𝑅𝑏 ↔ (◡𝐹‘𝑏)𝑅𝑏))
66		fveq2 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (◡𝐹‘𝑏) → (𝐹‘𝑐) = (𝐹‘(◡𝐹‘𝑏)))
67		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (◡𝐹‘𝑏) → 𝑐 = (◡𝐹‘𝑏))
68	66, 67	eqeq12d 2753	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (◡𝐹‘𝑏) → ((𝐹‘𝑐) = 𝑐 ↔ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)))
69	65, 68	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (◡𝐹‘𝑏) → ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ ((◡𝐹‘𝑏)𝑅𝑏 → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
70	69	rspcv 3575	. . . . . . . . . . . . . 14 ⊢ ((◡𝐹‘𝑏) ∈ 𝐴 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((◡𝐹‘𝑏)𝑅𝑏 → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
71	70	com23 86	. . . . . . . . . . . . 13 ⊢ ((◡𝐹‘𝑏) ∈ 𝐴 → ((◡𝐹‘𝑏)𝑅𝑏 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
72	57, 64, 71	sylc 65	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)))
73		simplrr 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → ¬ (𝐹‘𝑏) = 𝑏)
74		fveq2 6839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘(◡𝐹‘𝑏)))
75	74	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘(◡𝐹‘𝑏)))
76	61	fveq2d 6843	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘𝑏))
77	76	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘𝑏))
78	61	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
79	75, 77, 78	3eqtr3d 2785	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘𝑏) = 𝑏)
80	73, 79, 48	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
81	80	ex 413	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
82	81	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
83	72, 82	syld 47	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
84		simprr 771	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ¬ (𝐹‘𝑏) = 𝑏)
85		simpl1 1191	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑅 We 𝐴)
86		weso 5622	. . . . . . . . . . . . . . 15 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
87	85, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑅 Or 𝐴)
88		sotrieq 5572	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Or 𝐴 ∧ ((𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐹‘𝑏) = 𝑏 ↔ ¬ ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏))))
89	87, 34, 33, 88	syl12anc 835	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏) = 𝑏 ↔ ¬ ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏))))
90	89	con2bid 354	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏)) ↔ ¬ (𝐹‘𝑏) = 𝑏))
91	84, 90	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏)))
92	52, 83, 91	mpjaodan 957	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
93	27, 92	biimtrid 241	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
94	93	ex 413	. . . . . . . 8 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ((𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏) → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)))
95	18, 94	biimtrid 241	. . . . . . 7 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)))
96	95	rexlimdv 3148	. . . . . 6 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
97	13, 96	syld 47	. . . . 5 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
98	3, 97	biimtrrid 242	. . . 4 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
99	98	pm2.18d 127	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
100		fvresi 7115	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (( I ↾ 𝐴)‘𝑎) = 𝑎)
101	100	eqeq2d 2748	. . . . 5 ⊢ (𝑎 ∈ 𝐴 → ((𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎) ↔ (𝐹‘𝑎) = 𝑎))
102	101	biimprd 247	. . . 4 ⊢ (𝑎 ∈ 𝐴 → ((𝐹‘𝑎) = 𝑎 → (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
103	102	ralimia 3081	. . 3 ⊢ (∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎))
104	99, 103	syl 17	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎))
105	29	3ad2ant3 1135	. . . 4 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹:𝐴–1-1-onto→𝐴)
106		f1ofn 6782	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹 Fn 𝐴)
107	105, 106	syl 17	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 Fn 𝐴)
108		fnresi 6627	. . . 4 ⊢ ( I ↾ 𝐴) Fn 𝐴
109	108	a1i 11	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ( I ↾ 𝐴) Fn 𝐴)
110		eqfnfv 6979	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
111	107, 109, 110	syl2anc 584	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
112	104, 111	mpbird 256	1 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  ∃!wreu 3349  {crab 3405   ⊆ wss 3908  ∅c0 4280   class class class wbr 5103   I cid 5528   Or wor 5542   Se wse 5584   We wwe 5585  ^◡ccnv 5630   ↾ cres 5633   Fn wfn 6488  ⟶wf 6489  –1-1→wf1 6490  –1-1-onto→wf1o 6492  ‘cfv 6493   Isom wiso 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502

This theorem is referenced by:  weisoeq  7296  oiid  9435