Theorem weniso 7348

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 4385	. . . . . 6 ⊢ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ ↔ ∃𝑎 ∈ 𝐴 ¬ (𝐹‘𝑎) = 𝑎)
2		rexnal 3101	. . . . . 6 ⊢ (∃𝑎 ∈ 𝐴 ¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
3	1, 2	bitri 275	. . . . 5 ⊢ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ ↔ ¬ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
4		simpl1 1192	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → 𝑅 We 𝐴)
5		simpl2 1193	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → 𝑅 Se 𝐴)
6		ssrab2 4077	. . . . . . . . . 10 ⊢ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴
7	6	a1i 11	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴)
8		simpr 486	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅)
9		wereu2 5673	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ⊆ 𝐴 ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅)) → ∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
10	4, 5, 7, 8, 9	syl22anc 838	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → ∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
11		reurex 3381	. . . . . . . 8 ⊢ (∃!𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
12	10, 11	syl 17	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅) → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
13	12	ex 414	. . . . . 6 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ≠ ∅ → ∃𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎}∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏))
14		fveq2 6889	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏))
15		id 22	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → 𝑎 = 𝑏)
16	14, 15	eqeq12d 2749	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → ((𝐹‘𝑎) = 𝑎 ↔ (𝐹‘𝑏) = 𝑏))
17	16	notbid 318	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ (𝐹‘𝑏) = 𝑏))
18	17	elrab 3683	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ↔ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏))
19		fveq2 6889	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → (𝐹‘𝑎) = (𝐹‘𝑐))
20		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
21	19, 20	eqeq12d 2749	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → ((𝐹‘𝑎) = 𝑎 ↔ (𝐹‘𝑐) = 𝑐))
22	21	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (¬ (𝐹‘𝑎) = 𝑎 ↔ ¬ (𝐹‘𝑐) = 𝑐))
23	22	ralrab 3689	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ 𝐴 (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
24		con34b 316	. . . . . . . . . . . . 13 ⊢ ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
25	24	bicomi 223	. . . . . . . . . . . 12 ⊢ ((¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
26	25	ralbii 3094	. . . . . . . . . . 11 ⊢ (∀𝑐 ∈ 𝐴 (¬ (𝐹‘𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
27	23, 26	bitri 275	. . . . . . . . . 10 ⊢ (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐))
28		simpl3 1194	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴))
29		isof1o 7317	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) → 𝐹:𝐴–1-1-onto→𝐴)
30	28, 29	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴–1-1-onto→𝐴)
31		f1of 6831	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴⟶𝐴)
32	30, 31	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴⟶𝐴)
33		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑏 ∈ 𝐴)
34	32, 33	ffvelcdmd 7085	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘𝑏) ∈ 𝐴)
35		breq1 5151	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑏) → (𝑐𝑅𝑏 ↔ (𝐹‘𝑏)𝑅𝑏))
36		fveq2 6889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑏) → (𝐹‘𝑐) = (𝐹‘(𝐹‘𝑏)))
37		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑏) → 𝑐 = (𝐹‘𝑏))
38	36, 37	eqeq12d 2749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑏) → ((𝐹‘𝑐) = 𝑐 ↔ (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏)))
39	35, 38	imbi12d 345	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑏) → ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
40	39	rspcv 3609	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑏) ∈ 𝐴 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
41	34, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((𝐹‘𝑏)𝑅𝑏 → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
42	41	com23 86	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏)𝑅𝑏 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏))))
43	42	imp 408	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏)))
44		f1of1 6830	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹:𝐴–1-1→𝐴)
45	30, 44	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝐹:𝐴–1-1→𝐴)
46		f1fveq 7258	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴–1-1→𝐴 ∧ ((𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) ↔ (𝐹‘𝑏) = 𝑏))
47	45, 34, 33, 46	syl12anc 836	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) ↔ (𝐹‘𝑏) = 𝑏))
48		pm2.21 123	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝐹‘𝑏) = 𝑏 → ((𝐹‘𝑏) = 𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
49	48	ad2antll 728	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏) = 𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
50	47, 49	sylbid 239	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
51	50	adantr 482	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → ((𝐹‘(𝐹‘𝑏)) = (𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
52	43, 51	syld 47	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘𝑏)𝑅𝑏) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
53		f1ocnv 6843	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → ◡𝐹:𝐴–1-1-onto→𝐴)
54		f1of 6831	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹:𝐴–1-1-onto→𝐴 → ◡𝐹:𝐴⟶𝐴)
55	30, 53, 54	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ◡𝐹:𝐴⟶𝐴)
56	55, 33	ffvelcdmd 7085	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (◡𝐹‘𝑏) ∈ 𝐴)
57	56	adantr 482	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (◡𝐹‘𝑏) ∈ 𝐴)
58		isorel 7320	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) ∧ ((◡𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((◡𝐹‘𝑏)𝑅𝑏 ↔ (𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏)))
59	28, 56, 33, 58	syl12anc 836	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((◡𝐹‘𝑏)𝑅𝑏 ↔ (𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏)))
60		f1ocnvfv2 7272	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
61	30, 33, 60	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
62	61	breq1d 5158	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(◡𝐹‘𝑏))𝑅(𝐹‘𝑏) ↔ 𝑏𝑅(𝐹‘𝑏)))
63	59, 62	bitr2d 280	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝑏𝑅(𝐹‘𝑏) ↔ (◡𝐹‘𝑏)𝑅𝑏))
64	63	biimpa 478	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (◡𝐹‘𝑏)𝑅𝑏)
65		breq1 5151	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (◡𝐹‘𝑏) → (𝑐𝑅𝑏 ↔ (◡𝐹‘𝑏)𝑅𝑏))
66		fveq2 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (◡𝐹‘𝑏) → (𝐹‘𝑐) = (𝐹‘(◡𝐹‘𝑏)))
67		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (◡𝐹‘𝑏) → 𝑐 = (◡𝐹‘𝑏))
68	66, 67	eqeq12d 2749	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (◡𝐹‘𝑏) → ((𝐹‘𝑐) = 𝑐 ↔ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)))
69	65, 68	imbi12d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (◡𝐹‘𝑏) → ((𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) ↔ ((◡𝐹‘𝑏)𝑅𝑏 → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
70	69	rspcv 3609	. . . . . . . . . . . . . 14 ⊢ ((◡𝐹‘𝑏) ∈ 𝐴 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ((◡𝐹‘𝑏)𝑅𝑏 → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
71	70	com23 86	. . . . . . . . . . . . 13 ⊢ ((◡𝐹‘𝑏) ∈ 𝐴 → ((◡𝐹‘𝑏)𝑅𝑏 → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏))))
72	57, 64, 71	sylc 65	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)))
73		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → ¬ (𝐹‘𝑏) = 𝑏)
74		fveq2 6889	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘(◡𝐹‘𝑏)))
75	74	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘(◡𝐹‘𝑏)))
76	61	fveq2d 6893	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘𝑏))
77	76	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(𝐹‘(◡𝐹‘𝑏))) = (𝐹‘𝑏))
78	61	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘(◡𝐹‘𝑏)) = 𝑏)
79	75, 77, 78	3eqtr3d 2781	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → (𝐹‘𝑏) = 𝑏)
80	73, 79, 48	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ (𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)
81	80	ex 414	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
82	81	adantr 482	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → ((𝐹‘(◡𝐹‘𝑏)) = (◡𝐹‘𝑏) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
83	72, 82	syld 47	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹‘𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
84		simprr 772	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ¬ (𝐹‘𝑏) = 𝑏)
85		simpl1 1192	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑅 We 𝐴)
86		weso 5667	. . . . . . . . . . . . . . 15 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
87	85, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → 𝑅 Or 𝐴)
88		sotrieq 5617	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Or 𝐴 ∧ ((𝐹‘𝑏) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐹‘𝑏) = 𝑏 ↔ ¬ ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏))))
89	87, 34, 33, 88	syl12anc 836	. . . . . . . . . . . . 13 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏) = 𝑏 ↔ ¬ ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏))))
90	89	con2bid 355	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏)) ↔ ¬ (𝐹‘𝑏) = 𝑏))
91	84, 90	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → ((𝐹‘𝑏)𝑅𝑏 ∨ 𝑏𝑅(𝐹‘𝑏)))
92	52, 83, 91	mpjaodan 958	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ 𝐴 (𝑐𝑅𝑏 → (𝐹‘𝑐) = 𝑐) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
93	27, 92	biimtrid 241	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏)) → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎))
94	93	ex 414	. . . . . . . 8 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ((𝑏 ∈ 𝐴 ∧ ¬ (𝐹‘𝑏) = 𝑏) → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)))
95	18, 94	biimtrid 241	. . . . . . 7 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝑏 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} → (∀𝑐 ∈ {𝑎 ∈ 𝐴 ∣ ¬ (𝐹‘𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = 𝑎)))
96	95	rexlimdv 3154	. . . . . 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 7168	. . . . . 6 ⊢ (𝑎 ∈ 𝐴 → (( I ↾ 𝐴)‘𝑎) = 𝑎)
101	100	eqeq2d 2744	. . . . 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 1136	. . . 4 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹:𝐴–1-1-onto→𝐴)
106		f1ofn 6832	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹 Fn 𝐴)
107	105, 106	syl 17	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 Fn 𝐴)
108		fnresi 6677	. . . 4 ⊢ ( I ↾ 𝐴) Fn 𝐴
109	108	a1i 11	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ( I ↾ 𝐴) Fn 𝐴)
110		eqfnfv 7030	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
111	107, 109, 110	syl2anc 585	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = (( I ↾ 𝐴)‘𝑎)))
112	104, 111	mpbird 257	1 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  ∃!wreu 3375  {crab 3433   ⊆ wss 3948  ∅c0 4322   class class class wbr 5148   I cid 5573   Or wor 5587   Se wse 5629   We wwe 5630  ^◡ccnv 5675   ↾ cres 5678   Fn wfn 6536  ⟶wf 6537  –1-1→wf1 6538  –1-1-onto→wf1o 6540  ‘cfv 6541   Isom wiso 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550

This theorem is referenced by:  weisoeq  7349  oiid  9533