MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  weniso Structured version   Visualization version   GIF version

Theorem weniso 6644
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.
StepHypRef Expression
1 rabn0 3991 . . . . . 6 ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ ↔ ∃𝑎𝐴 ¬ (𝐹𝑎) = 𝑎)
2 rexnal 3024 . . . . . 6 (∃𝑎𝐴 ¬ (𝐹𝑎) = 𝑎 ↔ ¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
31, 2bitri 264 . . . . 5 ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ ↔ ¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
4 simpl1 1084 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → 𝑅 We 𝐴)
5 simpl2 1085 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → 𝑅 Se 𝐴)
6 ssrab2 3720 . . . . . . . . . 10 {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴
76a1i 11 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴)
8 simpr 476 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅)
9 wereu2 5140 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴 ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅)) → ∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
104, 5, 7, 8, 9syl22anc 1367 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → ∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
11 reurex 3190 . . . . . . . 8 (∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
1210, 11syl 17 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
1312ex 449 . . . . . 6 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏))
14 fveq2 6229 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
15 id 22 . . . . . . . . . . 11 (𝑎 = 𝑏𝑎 = 𝑏)
1614, 15eqeq12d 2666 . . . . . . . . . 10 (𝑎 = 𝑏 → ((𝐹𝑎) = 𝑎 ↔ (𝐹𝑏) = 𝑏))
1716notbid 307 . . . . . . . . 9 (𝑎 = 𝑏 → (¬ (𝐹𝑎) = 𝑎 ↔ ¬ (𝐹𝑏) = 𝑏))
1817elrab 3396 . . . . . . . 8 (𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ↔ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏))
19 fveq2 6229 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
20 id 22 . . . . . . . . . . . . . 14 (𝑎 = 𝑐𝑎 = 𝑐)
2119, 20eqeq12d 2666 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → ((𝐹𝑎) = 𝑎 ↔ (𝐹𝑐) = 𝑐))
2221notbid 307 . . . . . . . . . . . 12 (𝑎 = 𝑐 → (¬ (𝐹𝑎) = 𝑎 ↔ ¬ (𝐹𝑐) = 𝑐))
2322ralrab 3401 . . . . . . . . . . 11 (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐𝐴 (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
24 con34b 305 . . . . . . . . . . . . 13 ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
2524bicomi 214 . . . . . . . . . . . 12 ((¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
2625ralbii 3009 . . . . . . . . . . 11 (∀𝑐𝐴 (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ ∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
2723, 26bitri 264 . . . . . . . . . 10 (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
28 simpl3 1086 . . . . . . . . . . . . . . . . . 18 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴))
29 isof1o 6613 . . . . . . . . . . . . . . . . . 18 (𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) → 𝐹:𝐴1-1-onto𝐴)
3028, 29syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴1-1-onto𝐴)
31 f1of 6175 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴𝐴)
3230, 31syl 17 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴𝐴)
33 simprl 809 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑏𝐴)
3432, 33ffvelrnd 6400 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹𝑏) ∈ 𝐴)
35 breq1 4688 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → (𝑐𝑅𝑏 ↔ (𝐹𝑏)𝑅𝑏))
36 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝐹𝑏) → (𝐹𝑐) = (𝐹‘(𝐹𝑏)))
37 id 22 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝐹𝑏) → 𝑐 = (𝐹𝑏))
3836, 37eqeq12d 2666 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → ((𝐹𝑐) = 𝑐 ↔ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
3935, 38imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4039rspcv 3336 . . . . . . . . . . . . . . 15 ((𝐹𝑏) ∈ 𝐴 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4134, 40syl 17 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4241com23 86 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4342imp 444 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
44 f1of1 6174 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴1-1𝐴)
4530, 44syl 17 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴1-1𝐴)
46 f1fveq 6559 . . . . . . . . . . . . . . 15 ((𝐹:𝐴1-1𝐴 ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) ↔ (𝐹𝑏) = 𝑏))
4745, 34, 33, 46syl12anc 1364 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) ↔ (𝐹𝑏) = 𝑏))
48 pm2.21 120 . . . . . . . . . . . . . . 15 (¬ (𝐹𝑏) = 𝑏 → ((𝐹𝑏) = 𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
4948ad2antll 765 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏) = 𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5047, 49sylbid 230 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5150adantr 480 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5243, 51syld 47 . . . . . . . . . . 11 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
53 f1ocnv 6187 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴1-1-onto𝐴)
54 f1of 6175 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴𝐴)
5530, 53, 543syl 18 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴𝐴)
5655, 33ffvelrnd 6400 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹𝑏) ∈ 𝐴)
5756adantr 480 . . . . . . . . . . . . 13 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (𝐹𝑏) ∈ 𝐴)
58 isorel 6616 . . . . . . . . . . . . . . . 16 ((𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹𝑏)𝑅𝑏 ↔ (𝐹‘(𝐹𝑏))𝑅(𝐹𝑏)))
5928, 56, 33, 58syl12anc 1364 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏 ↔ (𝐹‘(𝐹𝑏))𝑅(𝐹𝑏)))
60 f1ocnvfv2 6573 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐴1-1-onto𝐴𝑏𝐴) → (𝐹‘(𝐹𝑏)) = 𝑏)
6130, 33, 60syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹‘(𝐹𝑏)) = 𝑏)
6261breq1d 4695 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏))𝑅(𝐹𝑏) ↔ 𝑏𝑅(𝐹𝑏)))
6359, 62bitr2d 269 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝑏𝑅(𝐹𝑏) ↔ (𝐹𝑏)𝑅𝑏))
6463biimpa 500 . . . . . . . . . . . . 13 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (𝐹𝑏)𝑅𝑏)
65 breq1 4688 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → (𝑐𝑅𝑏 ↔ (𝐹𝑏)𝑅𝑏))
66 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → (𝐹𝑐) = (𝐹‘(𝐹𝑏)))
67 id 22 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → 𝑐 = (𝐹𝑏))
6866, 67eqeq12d 2666 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → ((𝐹𝑐) = 𝑐 ↔ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
6965, 68imbi12d 333 . . . . . . . . . . . . . . 15 (𝑐 = (𝐹𝑏) → ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7069rspcv 3336 . . . . . . . . . . . . . 14 ((𝐹𝑏) ∈ 𝐴 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7170com23 86 . . . . . . . . . . . . 13 ((𝐹𝑏) ∈ 𝐴 → ((𝐹𝑏)𝑅𝑏 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7257, 64, 71sylc 65 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
73 simplrr 818 . . . . . . . . . . . . . . 15 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → ¬ (𝐹𝑏) = 𝑏)
74 fveq2 6229 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹‘(𝐹𝑏)))
7574adantl 481 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹‘(𝐹𝑏)))
7661fveq2d 6233 . . . . . . . . . . . . . . . . 17 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹𝑏))
7776adantr 480 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹𝑏))
7861adantr 480 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹𝑏)) = 𝑏)
7975, 77, 783eqtr3d 2693 . . . . . . . . . . . . . . 15 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹𝑏) = 𝑏)
8073, 79, 48sylc 65 . . . . . . . . . . . . . 14 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
8180ex 449 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
8281adantr 480 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
8372, 82syld 47 . . . . . . . . . . 11 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
84 simprr 811 . . . . . . . . . . . 12 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ¬ (𝐹𝑏) = 𝑏)
85 simpl1 1084 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑅 We 𝐴)
86 weso 5134 . . . . . . . . . . . . . . 15 (𝑅 We 𝐴𝑅 Or 𝐴)
8785, 86syl 17 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑅 Or 𝐴)
88 sotrieq 5091 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴 ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹𝑏) = 𝑏 ↔ ¬ ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏))))
8987, 34, 33, 88syl12anc 1364 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏) = 𝑏 ↔ ¬ ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏))))
9089con2bid 343 . . . . . . . . . . . 12 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏)) ↔ ¬ (𝐹𝑏) = 𝑏))
9184, 90mpbird 247 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏)))
9252, 83, 91mpjaodan 844 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9327, 92syl5bi 232 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9493ex 449 . . . . . . . 8 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ((𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏) → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)))
9518, 94syl5bi 232 . . . . . . 7 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)))
9695rexlimdv 3059 . . . . . 6 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9713, 96syld 47 . . . . 5 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
983, 97syl5bir 233 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9998pm2.18d 124 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
100 fvresi 6480 . . . . . 6 (𝑎𝐴 → (( I ↾ 𝐴)‘𝑎) = 𝑎)
101100eqeq2d 2661 . . . . 5 (𝑎𝐴 → ((𝐹𝑎) = (( I ↾ 𝐴)‘𝑎) ↔ (𝐹𝑎) = 𝑎))
102101biimprd 238 . . . 4 (𝑎𝐴 → ((𝐹𝑎) = 𝑎 → (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
103102ralimia 2979 . . 3 (∀𝑎𝐴 (𝐹𝑎) = 𝑎 → ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎))
10499, 103syl 17 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎))
105293ad2ant3 1104 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹:𝐴1-1-onto𝐴)
106 f1ofn 6176 . . . 4 (𝐹:𝐴1-1-onto𝐴𝐹 Fn 𝐴)
107105, 106syl 17 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 Fn 𝐴)
108 fnresi 6046 . . . 4 ( I ↾ 𝐴) Fn 𝐴
109108a1i 11 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ( I ↾ 𝐴) Fn 𝐴)
110 eqfnfv 6351 . . 3 ((𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
111107, 109, 110syl2anc 694 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
112104, 111mpbird 247 1 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  ∃!wreu 2943  {crab 2945  wss 3607  c0 3948   class class class wbr 4685   I cid 5052   Or wor 5063   Se wse 5100   We wwe 5101  ccnv 5142  cres 5145   Fn wfn 5921  wf 5922  1-1wf1 5923  1-1-ontowf1o 5925  cfv 5926   Isom wiso 5927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935
This theorem is referenced by:  weisoeq  6645  oiid  8487
  Copyright terms: Public domain W3C validator