Theorem weniso 7141

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 4286	. . . . . 6 ⊢ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ ↔ ∃𝑎 ∈ 𝐴 ¬ (𝐹‘𝑎) = 𝑎)
2		rexnal 3150	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 ¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
3	1, 2	bitri 278	. . . . 5 ⊢ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ ↔ ¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
4		simpl1 1193	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → 𝑅 We 𝐴)
5		simpl2 1194	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → 𝑅 Se 𝐴)
6		ssrab2 3979	. . . . . . . . . 10 ⊢ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴
7	6	a1i 11	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴)
8		simpr 488	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅)
9		wereu2 5533	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴 ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅)) → ∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
10	4, 5, 7, 8, 9	syl22anc 839	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → ∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
11		reurex 3328	. . . . . . . 8 ⊢ (∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
12	10, 11	syl 17	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
13	12	ex 416	. . . . . 6 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏))
14		fveq2 6695	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏))
15		id 22	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏)
16	14, 15	eqeq12d 2752	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → ((𝐹‘𝑎) = 𝑎 ↔ (𝐹‘𝑏) = 𝑏))
17	16	notbid 321	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ (𝐹‘𝑏) = 𝑏))
18	17	elrab 3591	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ↔ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏))
19		fveq2 6695	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
20		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
21	19, 20	eqeq12d 2752	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) = 𝑎 ↔ (𝐹‘𝑐) = 𝑐))
22	21	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ (𝐹‘𝑐) = 𝑐))
23	22	ralrab 3596	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ 𝐴 (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
24		con34b 319	. . . . . . . . . . . . 13 ⊢ ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
25	24	bicomi 227	. . . . . . . . . . . 12 ⊢ ((¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
26	25	ralbii 3078	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ 𝐴 (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
27	23, 26	bitri 278	. . . . . . . . . 10 ⊢ (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
28		simpl3 1195	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴))
29		isof1o 7110	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) → 𝐹:𝐴–1-1-onto→𝐴)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴–1-1-onto→𝐴)
31		f1of 6639	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴⟶𝐴)
32	30, 31	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴⟶𝐴)
33		simprl 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑏 ∈ 𝐴)
34	32, 33	ffvelrnd 6883	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘𝑏) ∈ 𝐴)
35		breq1 5042	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑏) → (𝑐𝑅𝑏 ↔ (𝐹‘𝑏)𝑅𝑏))
36		fveq2 6695	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑏) → (𝐹‘𝑐) = (𝐹‘(𝐹‘𝑏)))
37		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑏) → 𝑐 = (𝐹‘𝑏))
38	36, 37	eqeq12d 2752	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑏) → ((𝐹‘𝑐) = 𝑐 ↔ (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏)))
39	35, 38	imbi12d 348	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑏) → ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
40	39	rspcv 3522	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑏) ∈ 𝐴 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
41	34, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
42	41	com23 86	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏)𝑅𝑏 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
43	42	imp 410	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏)))
44		f1of1 6638	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴–1-1→𝐴)
45	30, 44	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴–1-1→𝐴)
46		f1fveq 7052	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴–1-1→𝐴 ∧ ((𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) ↔ (𝐹‘𝑏) = 𝑏))
47	45, 34, 33, 46	syl12anc 837	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) ↔ (𝐹‘𝑏) = 𝑏))
48		pm2.21 123	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝐹‘𝑏) = 𝑏 → ((𝐹‘𝑏) = 𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
49	48	ad2antll 729	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏) = 𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
50	47, 49	sylbid 243	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
51	50	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
52	43, 51	syld 47	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
53		f1ocnv 6651	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐴)
54		f1of 6639	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹:𝐴–1-1-onto→𝐴 → ◡𝐹:𝐴⟶𝐴)
55	30, 53, 54	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ◡𝐹:𝐴⟶𝐴)
56	55, 33	ffvelrnd 6883	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (◡𝐹‘𝑏) ∈ 𝐴)
57	56	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (◡𝐹‘𝑏) ∈ 𝐴)
58		isorel 7113	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) ∧ ((◡𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((◡𝐹‘𝑏)𝑅𝑏 ↔ (𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏)))
59	28, 56, 33, 58	syl12anc 837	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((◡𝐹‘𝑏)𝑅𝑏 ↔ (𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏)))
60		f1ocnvfv2 7066	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
61	30, 33, 60	syl2anc 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
62	61	breq1d 5049	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏) ↔ 𝑏𝑅(𝐹‘𝑏)))
63	59, 62	bitr2d 283	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝑏𝑅(𝐹‘𝑏) ↔ (◡𝐹‘𝑏)𝑅𝑏))
64	63	biimpa 480	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (◡𝐹‘𝑏)𝑅𝑏)
65		breq1 5042	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (◡𝐹‘𝑏) → (𝑐𝑅𝑏 ↔ (◡𝐹‘𝑏)𝑅𝑏))
66		fveq2 6695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (◡𝐹‘𝑏) → (𝐹‘𝑐) = (𝐹‘(◡𝐹‘𝑏)))
67		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (◡𝐹‘𝑏) → 𝑐 = (◡𝐹‘𝑏))
68	66, 67	eqeq12d 2752	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (◡𝐹‘𝑏) → ((𝐹‘𝑐) = 𝑐 ↔ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)))
69	65, 68	imbi12d 348	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (◡𝐹‘𝑏) → ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ ((◡𝐹‘𝑏)𝑅𝑏 → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
70	69	rspcv 3522	. . . . . . . . . . . . . 14 ⊢ ((◡𝐹‘𝑏) ∈ 𝐴 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((◡𝐹‘𝑏)𝑅𝑏 → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
71	70	com23 86	. . . . . . . . . . . . 13 ⊢ ((◡𝐹‘𝑏) ∈ 𝐴 → ((◡𝐹‘𝑏)𝑅𝑏 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
72	57, 64, 71	sylc 65	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)))
73		simplrr 778	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → ¬ (𝐹‘𝑏) = 𝑏)
74		fveq2 6695	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘(◡𝐹‘𝑏)))
75	74	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘(◡𝐹‘𝑏)))
76	61	fveq2d 6699	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘𝑏))
77	76	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘𝑏))
78	61	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
79	75, 77, 78	3eqtr3d 2779	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘𝑏) = 𝑏)
80	73, 79, 48	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
81	80	ex 416	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
82	81	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
83	72, 82	syld 47	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
84		simprr 773	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ¬ (𝐹‘𝑏) = 𝑏)
85		simpl1 1193	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑅 We 𝐴)
86		weso 5527	. . . . . . . . . . . . . . 15 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
87	85, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑅 Or 𝐴)
88		sotrieq 5482	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Or 𝐴 ∧ ((𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐹‘𝑏) = 𝑏 ↔ ¬ ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏))))
89	87, 34, 33, 88	syl12anc 837	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏) = 𝑏 ↔ ¬ ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏))))
90	89	con2bid 358	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏)) ↔ ¬ (𝐹‘𝑏) = 𝑏))
91	84, 90	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏)))
92	52, 83, 91	mpjaodan 959	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
93	27, 92	syl5bi 245	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
94	93	ex 416	. . . . . . . 8 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ((𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏) → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)))
95	18, 94	syl5bi 245	. . . . . . 7 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)))
96	95	rexlimdv 3192	. . . . . 6 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
97	13, 96	syld 47	. . . . 5 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
98	3, 97	syl5bir 246	. . . 4 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
99	98	pm2.18d 127	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
100		fvresi 6966	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (( I ↾ 𝐴)‘𝑎) = 𝑎)
101	100	eqeq2d 2747	. . . . 5 ⊢ (𝑎 ∈ 𝐴 → ((𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎) ↔ (𝐹‘𝑎) = 𝑎))
102	101	biimprd 251	. . . 4 ⊢ (𝑎 ∈ 𝐴 → ((𝐹‘𝑎) = 𝑎 → (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
103	102	ralimia 3071	. . 3 ⊢ (∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎))
104	99, 103	syl 17	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎))
105	29	3ad2ant3 1137	. . . 4 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹:𝐴–1-1-onto→𝐴)
106		f1ofn 6640	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹 Fn 𝐴)
107	105, 106	syl 17	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 Fn 𝐴)
108		fnresi 6484	. . . 4 ⊢ ( I ↾ 𝐴) Fn 𝐴
109	108	a1i 11	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ( I ↾ 𝐴) Fn 𝐴)
110		eqfnfv 6830	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
111	107, 109, 110	syl2anc 587	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
112	104, 111	mpbird 260	1 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 847   ∧ w3a 1089   = wceq 1543   ∈ wcel 2112   ≠ wne 2932  ∀wral 3051  ∃wrex 3052  ∃!wreu 3053  {crab 3055   ⊆ wss 3853  ∅c0 4223   class class class wbr 5039   I cid 5439   Or wor 5452   Se wse 5492   We wwe 5493  ^◡ccnv 5535   ↾ cres 5538   Fn wfn 6353  ⟶wf 6354  –1-1→wf1 6355  –1-1-onto→wf1o 6357  ‘cfv 6358   Isom wiso 6359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-po 5453  df-so 5454  df-fr 5494  df-se 5495  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-isom 6367

This theorem is referenced by:  weisoeq  7142  oiid  9135