Theorem weniso 7364

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 4339	. . . . . 6 ⊢ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ ↔ ∃𝑎 ∈ 𝐴 ¬ (𝐹‘𝑎) = 𝑎)
2		rexnal 3115	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 ¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
3	1, 2	bitri 278	. . . . 5 ⊢ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ ↔ ¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
4		simpl1 1210	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → 𝑅 We 𝐴)
5		simpl2 1211	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → 𝑅 Se 𝐴)
6		ssrab2 4028	. . . . . . . . . 10 ⊢ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴
7	6	a1i 11	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴)
8		simpr 490	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅)
9		wereu2 5648	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴 ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅)) → ∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
10	4, 5, 7, 8, 9	syl22anc 852	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → ∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
11		reurex 3370	. . . . . . . 8 ⊢ (∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
12	10, 11	syl 18	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
13	12	ex 418	. . . . . 6 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏))
14		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏))
15		id 23	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏)
16	14, 15	eqeq12d 2777	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → ((𝐹‘𝑎) = 𝑎 ↔ (𝐹‘𝑏) = 𝑏))
17	16	notbid 321	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ (𝐹‘𝑏) = 𝑏))
18	17	elrab 3645	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ↔ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏))
19		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
20		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
21	19, 20	eqeq12d 2777	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) = 𝑎 ↔ (𝐹‘𝑐) = 𝑐))
22	21	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ (𝐹‘𝑐) = 𝑐))
23	22	ralrab 3652	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ 𝐴 (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
24		con34b 319	. . . . . . . . . . . . 13 ⊢ ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
25	24	bicomi 227	. . . . . . . . . . . 12 ⊢ ((¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
26	25	ralbii 3109	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ 𝐴 (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
27	23, 26	bitri 278	. . . . . . . . . 10 ⊢ (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
28		simpl3 1212	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴))
29		isof1o 7331	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) → 𝐹:𝐴–1-1-onto→𝐴)
30	28, 29	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴–1-1-onto→𝐴)
31		f1of 6824	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴⟶𝐴)
32	30, 31	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴⟶𝐴)
33		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑏 ∈ 𝐴)
34	32, 33	ffvelcdmd 7085	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘𝑏) ∈ 𝐴)
35		breq1 5106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑏) → (𝑐𝑅𝑏 ↔ (𝐹‘𝑏)𝑅𝑏))
36		fveq2 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑏) → (𝐹‘𝑐) = (𝐹‘(𝐹‘𝑏)))
37		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑏) → 𝑐 = (𝐹‘𝑏))
38	36, 37	eqeq12d 2777	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑏) → ((𝐹‘𝑐) = 𝑐 ↔ (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏)))
39	35, 38	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑏) → ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
40	39	rspcv 3573	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑏) ∈ 𝐴 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
41	34, 40	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
42	41	com23 87	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏)𝑅𝑏 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
43	42	imp 412	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏)))
44		f1of1 6823	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴–1-1→𝐴)
45	30, 44	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴–1-1→𝐴)
46		f1fveq 7266	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴–1-1→𝐴 ∧ ((𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) ↔ (𝐹‘𝑏) = 𝑏))
47	45, 34, 33, 46	syl12anc 850	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) ↔ (𝐹‘𝑏) = 𝑏))
48		pm2.21 124	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝐹‘𝑏) = 𝑏 → ((𝐹‘𝑏) = 𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
49	48	ad2antll 742	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏) = 𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
50	47, 49	sylbid 243	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
51	50	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
52	43, 51	syld 48	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
53		f1ocnv 6837	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐴)
54		f1of 6824	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹:𝐴–1-1-onto→𝐴 → ◡𝐹:𝐴⟶𝐴)
55	30, 53, 54	3syl 19	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ◡𝐹:𝐴⟶𝐴)
56	55, 33	ffvelcdmd 7085	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (◡𝐹‘𝑏) ∈ 𝐴)
57	56	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (◡𝐹‘𝑏) ∈ 𝐴)
58		isorel 7334	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) ∧ ((◡𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((◡𝐹‘𝑏)𝑅𝑏 ↔ (𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏)))
59	28, 56, 33, 58	syl12anc 850	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((◡𝐹‘𝑏)𝑅𝑏 ↔ (𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏)))
60		f1ocnvfv2 7285	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
61	30, 33, 60	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
62	61	breq1d 5113	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏) ↔ 𝑏𝑅(𝐹‘𝑏)))
63	59, 62	bitr2d 283	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝑏𝑅(𝐹‘𝑏) ↔ (◡𝐹‘𝑏)𝑅𝑏))
64	63	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (◡𝐹‘𝑏)𝑅𝑏)
65		breq1 5106	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (◡𝐹‘𝑏) → (𝑐𝑅𝑏 ↔ (◡𝐹‘𝑏)𝑅𝑏))
66		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (◡𝐹‘𝑏) → (𝐹‘𝑐) = (𝐹‘(◡𝐹‘𝑏)))
67		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (◡𝐹‘𝑏) → 𝑐 = (◡𝐹‘𝑏))
68	66, 67	eqeq12d 2777	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (◡𝐹‘𝑏) → ((𝐹‘𝑐) = 𝑐 ↔ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)))
69	65, 68	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (◡𝐹‘𝑏) → ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ ((◡𝐹‘𝑏)𝑅𝑏 → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
70	69	rspcv 3573	. . . . . . . . . . . . . 14 ⊢ ((◡𝐹‘𝑏) ∈ 𝐴 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((◡𝐹‘𝑏)𝑅𝑏 → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
71	70	com23 87	. . . . . . . . . . . . 13 ⊢ ((◡𝐹‘𝑏) ∈ 𝐴 → ((◡𝐹‘𝑏)𝑅𝑏 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
72	57, 64, 71	sylc 66	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)))
73		simplrr 790	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → ¬ (𝐹‘𝑏) = 𝑏)
74		fveq2 6885	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘(◡𝐹‘𝑏)))
75	74	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘(◡𝐹‘𝑏)))
76	61	fveq2d 6889	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘𝑏))
77	76	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘𝑏))
78	61	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
79	75, 77, 78	3eqtr3d 2804	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘𝑏) = 𝑏)
80	73, 79, 48	sylc 66	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
81	80	ex 418	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
82	81	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
83	72, 82	syld 48	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
84		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ¬ (𝐹‘𝑏) = 𝑏)
85		simpl1 1210	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑅 We 𝐴)
86		weso 5642	. . . . . . . . . . . . . . 15 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
87	85, 86	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑅 Or 𝐴)
88		sotrieq 5590	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Or 𝐴 ∧ ((𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐹‘𝑏) = 𝑏 ↔ ¬ ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏))))
89	87, 34, 33, 88	syl12anc 850	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏) = 𝑏 ↔ ¬ ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏))))
90	89	con2bid 357	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏)) ↔ ¬ (𝐹‘𝑏) = 𝑏))
91	84, 90	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏)))
92	52, 83, 91	mpjaodan 973	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
93	27, 92	biimtrid 245	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
94	93	ex 418	. . . . . . . 8 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ((𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏) → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)))
95	18, 94	biimtrid 245	. . . . . . 7 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)))
96	95	rexlimdv 3162	. . . . . 6 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
97	13, 96	syld 48	. . . . 5 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
98	3, 97	biimtrrid 246	. . . 4 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
99	98	pm2.18d 128	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
100		fvresi 7178	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (( I ↾ 𝐴)‘𝑎) = 𝑎)
101	100	eqeq2d 2772	. . . . 5 ⊢ (𝑎 ∈ 𝐴 → ((𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎) ↔ (𝐹‘𝑎) = 𝑎))
102	101	biimprd 251	. . . 4 ⊢ (𝑎 ∈ 𝐴 → ((𝐹‘𝑎) = 𝑎 → (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
103	102	ralimia 3097	. . 3 ⊢ (∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎))
104	99, 103	syl 18	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎))
105	29	3ad2ant3 1153	. . . 4 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹:𝐴–1-1-onto→𝐴)
106		f1ofn 6825	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹 Fn 𝐴)
107	105, 106	syl 18	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 Fn 𝐴)
108		fnresi 6668	. . . 4 ⊢ ( I ↾ 𝐴) Fn 𝐴
109	108	a1i 11	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ( I ↾ 𝐴) Fn 𝐴)
110		eqfnfv 7029	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
111	107, 109, 110	syl2anc 596	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
112	104, 111	mpbird 260	1 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  ∃!wreu 3364  {crab 3413   ⊆ wss 3899  ∅c0 4279   class class class wbr 5103   I cid 5545   Or wor 5558   Se wse 5602   We wwe 5603  ^◡ccnv 5650   ↾ cres 5653   Fn wfn 6533  ⟶wf 6534  –1-1→wf1 6535  –1-1-onto→wf1o 6537  ‘cfv 6538   Isom wiso 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547

This theorem is used by:  weisoeq  7365  oiid  9535