Theorem weniso 7205

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 4316	. . . . . 6 ⊢ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ ↔ ∃𝑎 ∈ 𝐴 ¬ (𝐹‘𝑎) = 𝑎)
2		rexnal 3165	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 ¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
3	1, 2	bitri 274	. . . . 5 ⊢ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ ↔ ¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
4		simpl1 1189	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → 𝑅 We 𝐴)
5		simpl2 1190	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → 𝑅 Se 𝐴)
6		ssrab2 4009	. . . . . . . . . 10 ⊢ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴
7	6	a1i 11	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴)
8		simpr 484	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅)
9		wereu2 5577	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴 ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅)) → ∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
10	4, 5, 7, 8, 9	syl22anc 835	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → ∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
11		reurex 3352	. . . . . . . 8 ⊢ (∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
12	10, 11	syl 17	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
13	12	ex 412	. . . . . 6 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏))
14		fveq2 6756	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏))
15		id 22	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏)
16	14, 15	eqeq12d 2754	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → ((𝐹‘𝑎) = 𝑎 ↔ (𝐹‘𝑏) = 𝑏))
17	16	notbid 317	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ (𝐹‘𝑏) = 𝑏))
18	17	elrab 3617	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ↔ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏))
19		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
20		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
21	19, 20	eqeq12d 2754	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) = 𝑎 ↔ (𝐹‘𝑐) = 𝑐))
22	21	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ (𝐹‘𝑐) = 𝑐))
23	22	ralrab 3623	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ 𝐴 (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
24		con34b 315	. . . . . . . . . . . . 13 ⊢ ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
25	24	bicomi 223	. . . . . . . . . . . 12 ⊢ ((¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
26	25	ralbii 3090	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ 𝐴 (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
27	23, 26	bitri 274	. . . . . . . . . 10 ⊢ (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
28		simpl3 1191	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴))
29		isof1o 7174	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) → 𝐹:𝐴–1-1-onto→𝐴)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴–1-1-onto→𝐴)
31		f1of 6700	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴⟶𝐴)
32	30, 31	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴⟶𝐴)
33		simprl 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑏 ∈ 𝐴)
34	32, 33	ffvelrnd 6944	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘𝑏) ∈ 𝐴)
35		breq1 5073	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑏) → (𝑐𝑅𝑏 ↔ (𝐹‘𝑏)𝑅𝑏))
36		fveq2 6756	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑏) → (𝐹‘𝑐) = (𝐹‘(𝐹‘𝑏)))
37		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑏) → 𝑐 = (𝐹‘𝑏))
38	36, 37	eqeq12d 2754	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑏) → ((𝐹‘𝑐) = 𝑐 ↔ (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏)))
39	35, 38	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑏) → ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
40	39	rspcv 3547	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑏) ∈ 𝐴 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
41	34, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
42	41	com23 86	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏)𝑅𝑏 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
43	42	imp 406	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏)))
44		f1of1 6699	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴–1-1→𝐴)
45	30, 44	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴–1-1→𝐴)
46		f1fveq 7116	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴–1-1→𝐴 ∧ ((𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) ↔ (𝐹‘𝑏) = 𝑏))
47	45, 34, 33, 46	syl12anc 833	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) ↔ (𝐹‘𝑏) = 𝑏))
48		pm2.21 123	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝐹‘𝑏) = 𝑏 → ((𝐹‘𝑏) = 𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
49	48	ad2antll 725	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏) = 𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
50	47, 49	sylbid 239	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
51	50	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
52	43, 51	syld 47	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
53		f1ocnv 6712	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐴)
54		f1of 6700	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹:𝐴–1-1-onto→𝐴 → ◡𝐹:𝐴⟶𝐴)
55	30, 53, 54	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ◡𝐹:𝐴⟶𝐴)
56	55, 33	ffvelrnd 6944	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (◡𝐹‘𝑏) ∈ 𝐴)
57	56	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (◡𝐹‘𝑏) ∈ 𝐴)
58		isorel 7177	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) ∧ ((◡𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((◡𝐹‘𝑏)𝑅𝑏 ↔ (𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏)))
59	28, 56, 33, 58	syl12anc 833	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((◡𝐹‘𝑏)𝑅𝑏 ↔ (𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏)))
60		f1ocnvfv2 7130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
61	30, 33, 60	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
62	61	breq1d 5080	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏) ↔ 𝑏𝑅(𝐹‘𝑏)))
63	59, 62	bitr2d 279	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝑏𝑅(𝐹‘𝑏) ↔ (◡𝐹‘𝑏)𝑅𝑏))
64	63	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (◡𝐹‘𝑏)𝑅𝑏)
65		breq1 5073	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (◡𝐹‘𝑏) → (𝑐𝑅𝑏 ↔ (◡𝐹‘𝑏)𝑅𝑏))
66		fveq2 6756	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (◡𝐹‘𝑏) → (𝐹‘𝑐) = (𝐹‘(◡𝐹‘𝑏)))
67		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (◡𝐹‘𝑏) → 𝑐 = (◡𝐹‘𝑏))
68	66, 67	eqeq12d 2754	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (◡𝐹‘𝑏) → ((𝐹‘𝑐) = 𝑐 ↔ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)))
69	65, 68	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (◡𝐹‘𝑏) → ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ ((◡𝐹‘𝑏)𝑅𝑏 → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
70	69	rspcv 3547	. . . . . . . . . . . . . 14 ⊢ ((◡𝐹‘𝑏) ∈ 𝐴 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((◡𝐹‘𝑏)𝑅𝑏 → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
71	70	com23 86	. . . . . . . . . . . . 13 ⊢ ((◡𝐹‘𝑏) ∈ 𝐴 → ((◡𝐹‘𝑏)𝑅𝑏 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
72	57, 64, 71	sylc 65	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)))
73		simplrr 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → ¬ (𝐹‘𝑏) = 𝑏)
74		fveq2 6756	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘(◡𝐹‘𝑏)))
75	74	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘(◡𝐹‘𝑏)))
76	61	fveq2d 6760	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘𝑏))
77	76	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘𝑏))
78	61	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
79	75, 77, 78	3eqtr3d 2786	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘𝑏) = 𝑏)
80	73, 79, 48	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
81	80	ex 412	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
82	81	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
83	72, 82	syld 47	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
84		simprr 769	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ¬ (𝐹‘𝑏) = 𝑏)
85		simpl1 1189	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑅 We 𝐴)
86		weso 5571	. . . . . . . . . . . . . . 15 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
87	85, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑅 Or 𝐴)
88		sotrieq 5523	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Or 𝐴 ∧ ((𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐹‘𝑏) = 𝑏 ↔ ¬ ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏))))
89	87, 34, 33, 88	syl12anc 833	. . . . . . . . . . . . 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 955	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
93	27, 92	syl5bi 241	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
94	93	ex 412	. . . . . . . 8 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ((𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏) → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)))
95	18, 94	syl5bi 241	. . . . . . 7 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)))
96	95	rexlimdv 3211	. . . . . 6 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
97	13, 96	syld 47	. . . . 5 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
98	3, 97	syl5bir 242	. . . 4 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
99	98	pm2.18d 127	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
100		fvresi 7027	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (( I ↾ 𝐴)‘𝑎) = 𝑎)
101	100	eqeq2d 2749	. . . . 5 ⊢ (𝑎 ∈ 𝐴 → ((𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎) ↔ (𝐹‘𝑎) = 𝑎))
102	101	biimprd 247	. . . 4 ⊢ (𝑎 ∈ 𝐴 → ((𝐹‘𝑎) = 𝑎 → (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
103	102	ralimia 3084	. . 3 ⊢ (∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎))
104	99, 103	syl 17	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎))
105	29	3ad2ant3 1133	. . . 4 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹:𝐴–1-1-onto→𝐴)
106		f1ofn 6701	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹 Fn 𝐴)
107	105, 106	syl 17	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 Fn 𝐴)
108		fnresi 6545	. . . 4 ⊢ ( I ↾ 𝐴) Fn 𝐴
109	108	a1i 11	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ( I ↾ 𝐴) Fn 𝐴)
110		eqfnfv 6891	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
111	107, 109, 110	syl2anc 583	. 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 395   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  ∃!wreu 3065  {crab 3067   ⊆ wss 3883  ∅c0 4253   class class class wbr 5070   I cid 5479   Or wor 5493   Se wse 5533   We wwe 5534  ^◡ccnv 5579   ↾ cres 5582   Fn wfn 6413  ⟶wf 6414  –1-1→wf1 6415  –1-1-onto→wf1o 6417  ‘cfv 6418   Isom wiso 6419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427

This theorem is referenced by:  weisoeq  7206  oiid  9230