Metamath Proof Explorer

Theorem weniso

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)

Ref Expression
Assertion weniso ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → 𝐹 = ( I ↾ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rabn0 ⊢ ( { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ ↔ ∃ 𝑎 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 )
2 rexnal ⊢ ( ∃ 𝑎 ∈ 𝐴 ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 ↔ ¬ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 )
3 1 2 bitri ⊢ ( { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ ↔ ¬ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 )
4 simpl1 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ ) → 𝑅 We 𝐴 )
5 simpl2 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ ) → 𝑅 Se 𝐴 )
6 ssrab2 ⊢ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ⊆ 𝐴
7 6 a1i ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ ) → { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ⊆ 𝐴 )
8 simpr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ ) → { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ )
9 wereu2 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ⊆ 𝐴 ∧ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ ) ) → ∃! 𝑏 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 )
10 4 5 7 8 9 syl22anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ ) → ∃! 𝑏 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 )
11 reurex ⊢ ( ∃! 𝑏 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 → ∃ 𝑏 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 )
12 10 11 syl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ ) → ∃ 𝑏 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 )
13 12 ex ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ( { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ → ∃ 𝑏 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 ) )
14 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) )
15 id ⊢ ( 𝑎 = 𝑏 → 𝑎 = 𝑏 )
16 14 15 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐹 ‘ 𝑎 ) = 𝑎 ↔ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) )
17 16 notbid ⊢ ( 𝑎 = 𝑏 → ( ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 ↔ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) )
18 17 elrab ⊢ ( 𝑏 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ↔ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) )
19 fveq2 ⊢ ( 𝑎 = 𝑐 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑐 ) )
20 id ⊢ ( 𝑎 = 𝑐 → 𝑎 = 𝑐 )
21 19 20 eqeq12d ⊢ ( 𝑎 = 𝑐 → ( ( 𝐹 ‘ 𝑎 ) = 𝑎 ↔ ( 𝐹 ‘ 𝑐 ) = 𝑐 ) )
22 21 notbid ⊢ ( 𝑎 = 𝑐 → ( ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 ↔ ¬ ( 𝐹 ‘ 𝑐 ) = 𝑐 ) )
23 22 ralrab ⊢ ( ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 ↔ ∀ 𝑐 ∈ 𝐴 ( ¬ ( 𝐹 ‘ 𝑐 ) = 𝑐 → ¬ 𝑐 𝑅 𝑏 ) )
24 con34b ⊢ ( ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) ↔ ( ¬ ( 𝐹 ‘ 𝑐 ) = 𝑐 → ¬ 𝑐 𝑅 𝑏 ) )
25 24 bicomi ⊢ ( ( ¬ ( 𝐹 ‘ 𝑐 ) = 𝑐 → ¬ 𝑐 𝑅 𝑏 ) ↔ ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) )
26 25 ralbii ⊢ ( ∀ 𝑐 ∈ 𝐴 ( ¬ ( 𝐹 ‘ 𝑐 ) = 𝑐 → ¬ 𝑐 𝑅 𝑏 ) ↔ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) )
27 23 26 bitri ⊢ ( ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 ↔ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) )
28 simpl3 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) )
29 isof1o ⊢ ( 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )
30 28 29 syl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )
31 f1of ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 : 𝐴 ⟶ 𝐴 )
32 30 31 syl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → 𝐹 : 𝐴 ⟶ 𝐴 )
33 simprl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → 𝑏 ∈ 𝐴 )
34 32 33 ffvelrnd ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ 𝐴 )
35 breq1 ⊢ ( 𝑐 = ( 𝐹 ‘ 𝑏 ) → ( 𝑐 𝑅 𝑏 ↔ ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ) )
36 fveq2 ⊢ ( 𝑐 = ( 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) )
37 id ⊢ ( 𝑐 = ( 𝐹 ‘ 𝑏 ) → 𝑐 = ( 𝐹 ‘ 𝑏 ) )
38 36 37 eqeq12d ⊢ ( 𝑐 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑐 ) = 𝑐 ↔ ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) ) )
39 35 38 imbi12d ⊢ ( 𝑐 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) ↔ ( ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 → ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) ) ) )
40 39 rspcv ⊢ ( ( 𝐹 ‘ 𝑏 ) ∈ 𝐴 → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) → ( ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 → ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) ) ) )
41 34 40 syl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) → ( ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 → ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) ) ) )
42 41 com23 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) ) ) )
43 42 imp ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ) → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) ) )
44 f1of1 ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 : 𝐴 –1-1→ 𝐴 )
45 30 44 syl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → 𝐹 : 𝐴 –1-1→ 𝐴 )
46 f1fveq ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐴 ∧ ( ( 𝐹 ‘ 𝑏 ) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) )
47 45 34 33 46 syl12anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) )
48 pm2.21 ⊢ ( ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 → ( ( 𝐹 ‘ 𝑏 ) = 𝑏 → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
49 48 ad2antll ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ( 𝐹 ‘ 𝑏 ) = 𝑏 → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
50 47 49 sylbid ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
51 50 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ) → ( ( 𝐹 ‘ ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ 𝑏 ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
52 43 51 syld ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ) → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
53 f1ocnv ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐴 )
54 f1of ⊢ ( ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 ⟶ 𝐴 )
55 30 53 54 3syl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ◡ 𝐹 : 𝐴 ⟶ 𝐴 )
56 55 33 ffvelrnd ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝐴 )
57 56 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ) → ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝐴 )
58 isorel ⊢ ( ( 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ∧ ( ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( ◡ 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) 𝑅 ( 𝐹 ‘ 𝑏 ) ) )
59 28 56 33 58 syl12anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ( ◡ 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) 𝑅 ( 𝐹 ‘ 𝑏 ) ) )
60 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = 𝑏 )
61 30 33 60 syl2anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = 𝑏 )
62 61 breq1d ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) 𝑅 ( 𝐹 ‘ 𝑏 ) ↔ 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ) )
63 59 62 bitr2d ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ↔ ( ◡ 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ) )
64 63 biimpa ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ) → ( ◡ 𝐹 ‘ 𝑏 ) 𝑅 𝑏 )
65 breq1 ⊢ ( 𝑐 = ( ◡ 𝐹 ‘ 𝑏 ) → ( 𝑐 𝑅 𝑏 ↔ ( ◡ 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ) )
66 fveq2 ⊢ ( 𝑐 = ( ◡ 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ 𝑐 ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) )
67 id ⊢ ( 𝑐 = ( ◡ 𝐹 ‘ 𝑏 ) → 𝑐 = ( ◡ 𝐹 ‘ 𝑏 ) )
68 66 67 eqeq12d ⊢ ( 𝑐 = ( ◡ 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑐 ) = 𝑐 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) )
69 65 68 imbi12d ⊢ ( 𝑐 = ( ◡ 𝐹 ‘ 𝑏 ) → ( ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) ↔ ( ( ◡ 𝐹 ‘ 𝑏 ) 𝑅 𝑏 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) ) )
70 69 rspcv ⊢ ( ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝐴 → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) → ( ( ◡ 𝐹 ‘ 𝑏 ) 𝑅 𝑏 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) ) )
71 70 com23 ⊢ ( ( ◡ 𝐹 ‘ 𝑏 ) ∈ 𝐴 → ( ( ◡ 𝐹 ‘ 𝑏 ) 𝑅 𝑏 → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) ) )
72 57 64 71 sylc ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ) → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) )
73 simplrr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) → ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 )
74 fveq2 ⊢ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) )
75 74 adantl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) )
76 61 fveq2d ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝐹 ‘ 𝑏 ) )
77 76 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) ) = ( 𝐹 ‘ 𝑏 ) )
78 61 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = 𝑏 )
79 75 77 78 3eqtr3d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) → ( 𝐹 ‘ 𝑏 ) = 𝑏 )
80 73 79 48 sylc ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 )
81 80 ex ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
82 81 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑏 ) ) = ( ◡ 𝐹 ‘ 𝑏 ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
83 72 82 syld ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) ∧ 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ) → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
84 simprr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 )
85 simpl1 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → 𝑅 We 𝐴 )
86 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
87 85 86 syl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → 𝑅 Or 𝐴 )
88 sotrieq ⊢ ( ( 𝑅 Or 𝐴 ∧ ( ( 𝐹 ‘ 𝑏 ) ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑏 ) = 𝑏 ↔ ¬ ( ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ∨ 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ) ) )
89 87 34 33 88 syl12anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ( 𝐹 ‘ 𝑏 ) = 𝑏 ↔ ¬ ( ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ∨ 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ) ) )
90 89 con2bid ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ( ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ∨ 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ) ↔ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) )
91 84 90 mpbird ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ( 𝐹 ‘ 𝑏 ) 𝑅 𝑏 ∨ 𝑏 𝑅 ( 𝐹 ‘ 𝑏 ) ) )
92 52 83 91 mpjaodan ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝐹 ‘ 𝑐 ) = 𝑐 ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
93 27 92 syl5bi ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) ) → ( ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
94 93 ex ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ( ( 𝑏 ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑏 ) = 𝑏 ) → ( ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) ) )
95 18 94 syl5bi ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ( 𝑏 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } → ( ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) ) )
96 95 rexlimdv ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ( ∃ 𝑏 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ∀ 𝑐 ∈ { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ¬ 𝑐 𝑅 𝑏 → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
97 13 96 syld ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ( { 𝑎 ∈ 𝐴 ∣ ¬ ( 𝐹 ‘ 𝑎 ) = 𝑎 } ≠ ∅ → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
98 3 97 syl5bir ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ( ¬ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
99 98 pm2.18d ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 )
100 fvresi ⊢ ( 𝑎 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑎 ) = 𝑎 )
101 100 eqeq2d ⊢ ( 𝑎 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑎 ) = ( ( I ↾ 𝐴 ) ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝑎 ) = 𝑎 ) )
102 101 biimprd ⊢ ( 𝑎 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑎 ) = 𝑎 → ( 𝐹 ‘ 𝑎 ) = ( ( I ↾ 𝐴 ) ‘ 𝑎 ) ) )
103 102 ralimia ⊢ ( ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑎 → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( I ↾ 𝐴 ) ‘ 𝑎 ) )
104 99 103 syl ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( I ↾ 𝐴 ) ‘ 𝑎 ) )
105 29 3ad2ant3 ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → 𝐹 : 𝐴 –1-1-onto→ 𝐴 )
106 f1ofn ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 Fn 𝐴 )
107 105 106 syl ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → 𝐹 Fn 𝐴 )
108 fnresi ⊢ ( I ↾ 𝐴 ) Fn 𝐴
109 108 a1i ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ( I ↾ 𝐴 ) Fn 𝐴 )
110 eqfnfv ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴 ) Fn 𝐴 ) → ( 𝐹 = ( I ↾ 𝐴 ) ↔ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( I ↾ 𝐴 ) ‘ 𝑎 ) ) )
111 107 109 110 syl2anc ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → ( 𝐹 = ( I ↾ 𝐴 ) ↔ ∀ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ( ( I ↾ 𝐴 ) ‘ 𝑎 ) ) )
112 104 111 mpbird ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ) → 𝐹 = ( I ↾ 𝐴 ) )