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

Theorem weniso 7299
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 4345 . . . . . 6 ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ ↔ ∃𝑎𝐴 ¬ (𝐹𝑎) = 𝑎)
2 rexnal 3103 . . . . . 6 (∃𝑎𝐴 ¬ (𝐹𝑎) = 𝑎 ↔ ¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
31, 2bitri 274 . . . . 5 ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ ↔ ¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
4 simpl1 1191 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → 𝑅 We 𝐴)
5 simpl2 1192 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → 𝑅 Se 𝐴)
6 ssrab2 4037 . . . . . . . . . 10 {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴
76a1i 11 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴)
8 simpr 485 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅)
9 wereu2 5630 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴 ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅)) → ∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
104, 5, 7, 8, 9syl22anc 837 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → ∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
11 reurex 3357 . . . . . . . 8 (∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
1210, 11syl 17 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
1312ex 413 . . . . . 6 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏))
14 fveq2 6842 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
15 id 22 . . . . . . . . . . 11 (𝑎 = 𝑏𝑎 = 𝑏)
1614, 15eqeq12d 2752 . . . . . . . . . 10 (𝑎 = 𝑏 → ((𝐹𝑎) = 𝑎 ↔ (𝐹𝑏) = 𝑏))
1716notbid 317 . . . . . . . . 9 (𝑎 = 𝑏 → (¬ (𝐹𝑎) = 𝑎 ↔ ¬ (𝐹𝑏) = 𝑏))
1817elrab 3645 . . . . . . . 8 (𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ↔ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏))
19 fveq2 6842 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
20 id 22 . . . . . . . . . . . . . 14 (𝑎 = 𝑐𝑎 = 𝑐)
2119, 20eqeq12d 2752 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → ((𝐹𝑎) = 𝑎 ↔ (𝐹𝑐) = 𝑐))
2221notbid 317 . . . . . . . . . . . 12 (𝑎 = 𝑐 → (¬ (𝐹𝑎) = 𝑎 ↔ ¬ (𝐹𝑐) = 𝑐))
2322ralrab 3651 . . . . . . . . . . 11 (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐𝐴 (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
24 con34b 315 . . . . . . . . . . . . 13 ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
2524bicomi 223 . . . . . . . . . . . 12 ((¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
2625ralbii 3096 . . . . . . . . . . 11 (∀𝑐𝐴 (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ ∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
2723, 26bitri 274 . . . . . . . . . 10 (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
28 simpl3 1193 . . . . . . . . . . . . . . . . . 18 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴))
29 isof1o 7268 . . . . . . . . . . . . . . . . . 18 (𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) → 𝐹:𝐴1-1-onto𝐴)
3028, 29syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴1-1-onto𝐴)
31 f1of 6784 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴𝐴)
3230, 31syl 17 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴𝐴)
33 simprl 769 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑏𝐴)
3432, 33ffvelcdmd 7036 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹𝑏) ∈ 𝐴)
35 breq1 5108 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → (𝑐𝑅𝑏 ↔ (𝐹𝑏)𝑅𝑏))
36 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝐹𝑏) → (𝐹𝑐) = (𝐹‘(𝐹𝑏)))
37 id 22 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝐹𝑏) → 𝑐 = (𝐹𝑏))
3836, 37eqeq12d 2752 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → ((𝐹𝑐) = 𝑐 ↔ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
3935, 38imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4039rspcv 3577 . . . . . . . . . . . . . . 15 ((𝐹𝑏) ∈ 𝐴 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4134, 40syl 17 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4241com23 86 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4342imp 407 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
44 f1of1 6783 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴1-1𝐴)
4530, 44syl 17 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴1-1𝐴)
46 f1fveq 7209 . . . . . . . . . . . . . . 15 ((𝐹:𝐴1-1𝐴 ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) ↔ (𝐹𝑏) = 𝑏))
4745, 34, 33, 46syl12anc 835 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) ↔ (𝐹𝑏) = 𝑏))
48 pm2.21 123 . . . . . . . . . . . . . . 15 (¬ (𝐹𝑏) = 𝑏 → ((𝐹𝑏) = 𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
4948ad2antll 727 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏) = 𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5047, 49sylbid 239 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5150adantr 481 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5243, 51syld 47 . . . . . . . . . . 11 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
53 f1ocnv 6796 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴1-1-onto𝐴)
54 f1of 6784 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴𝐴)
5530, 53, 543syl 18 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴𝐴)
5655, 33ffvelcdmd 7036 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹𝑏) ∈ 𝐴)
5756adantr 481 . . . . . . . . . . . . 13 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (𝐹𝑏) ∈ 𝐴)
58 isorel 7271 . . . . . . . . . . . . . . . 16 ((𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹𝑏)𝑅𝑏 ↔ (𝐹‘(𝐹𝑏))𝑅(𝐹𝑏)))
5928, 56, 33, 58syl12anc 835 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏 ↔ (𝐹‘(𝐹𝑏))𝑅(𝐹𝑏)))
60 f1ocnvfv2 7223 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐴1-1-onto𝐴𝑏𝐴) → (𝐹‘(𝐹𝑏)) = 𝑏)
6130, 33, 60syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹‘(𝐹𝑏)) = 𝑏)
6261breq1d 5115 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏))𝑅(𝐹𝑏) ↔ 𝑏𝑅(𝐹𝑏)))
6359, 62bitr2d 279 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝑏𝑅(𝐹𝑏) ↔ (𝐹𝑏)𝑅𝑏))
6463biimpa 477 . . . . . . . . . . . . 13 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (𝐹𝑏)𝑅𝑏)
65 breq1 5108 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → (𝑐𝑅𝑏 ↔ (𝐹𝑏)𝑅𝑏))
66 fveq2 6842 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → (𝐹𝑐) = (𝐹‘(𝐹𝑏)))
67 id 22 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → 𝑐 = (𝐹𝑏))
6866, 67eqeq12d 2752 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → ((𝐹𝑐) = 𝑐 ↔ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
6965, 68imbi12d 344 . . . . . . . . . . . . . . 15 (𝑐 = (𝐹𝑏) → ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7069rspcv 3577 . . . . . . . . . . . . . 14 ((𝐹𝑏) ∈ 𝐴 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7170com23 86 . . . . . . . . . . . . 13 ((𝐹𝑏) ∈ 𝐴 → ((𝐹𝑏)𝑅𝑏 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7257, 64, 71sylc 65 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
73 simplrr 776 . . . . . . . . . . . . . . 15 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → ¬ (𝐹𝑏) = 𝑏)
74 fveq2 6842 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹‘(𝐹𝑏)))
7574adantl 482 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹‘(𝐹𝑏)))
7661fveq2d 6846 . . . . . . . . . . . . . . . . 17 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹𝑏))
7776adantr 481 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹𝑏))
7861adantr 481 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹𝑏)) = 𝑏)
7975, 77, 783eqtr3d 2784 . . . . . . . . . . . . . . 15 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹𝑏) = 𝑏)
8073, 79, 48sylc 65 . . . . . . . . . . . . . 14 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
8180ex 413 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
8281adantr 481 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
8372, 82syld 47 . . . . . . . . . . 11 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
84 simprr 771 . . . . . . . . . . . 12 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ¬ (𝐹𝑏) = 𝑏)
85 simpl1 1191 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑅 We 𝐴)
86 weso 5624 . . . . . . . . . . . . . . 15 (𝑅 We 𝐴𝑅 Or 𝐴)
8785, 86syl 17 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑅 Or 𝐴)
88 sotrieq 5574 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴 ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹𝑏) = 𝑏 ↔ ¬ ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏))))
8987, 34, 33, 88syl12anc 835 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏) = 𝑏 ↔ ¬ ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏))))
9089con2bid 354 . . . . . . . . . . . 12 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏)) ↔ ¬ (𝐹𝑏) = 𝑏))
9184, 90mpbird 256 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏)))
9252, 83, 91mpjaodan 957 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9327, 92biimtrid 241 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9493ex 413 . . . . . . . 8 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ((𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏) → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)))
9518, 94biimtrid 241 . . . . . . 7 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)))
9695rexlimdv 3150 . . . . . 6 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9713, 96syld 47 . . . . 5 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
983, 97biimtrrid 242 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9998pm2.18d 127 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
100 fvresi 7119 . . . . . 6 (𝑎𝐴 → (( I ↾ 𝐴)‘𝑎) = 𝑎)
101100eqeq2d 2747 . . . . 5 (𝑎𝐴 → ((𝐹𝑎) = (( I ↾ 𝐴)‘𝑎) ↔ (𝐹𝑎) = 𝑎))
102101biimprd 247 . . . 4 (𝑎𝐴 → ((𝐹𝑎) = 𝑎 → (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
103102ralimia 3083 . . 3 (∀𝑎𝐴 (𝐹𝑎) = 𝑎 → ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎))
10499, 103syl 17 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎))
105293ad2ant3 1135 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹:𝐴1-1-onto𝐴)
106 f1ofn 6785 . . . 4 (𝐹:𝐴1-1-onto𝐴𝐹 Fn 𝐴)
107105, 106syl 17 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 Fn 𝐴)
108 fnresi 6630 . . . 4 ( I ↾ 𝐴) Fn 𝐴
109108a1i 11 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ( I ↾ 𝐴) Fn 𝐴)
110 eqfnfv 6982 . . 3 ((𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
111107, 109, 110syl2anc 584 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
112104, 111mpbird 256 1 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  ∃!wreu 3351  {crab 3407  wss 3910  c0 4282   class class class wbr 5105   I cid 5530   Or wor 5544   Se wse 5586   We wwe 5587  ccnv 5632  cres 5635   Fn wfn 6491  wf 6492  1-1wf1 6493  1-1-ontowf1o 6495  cfv 6496   Isom wiso 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505
This theorem is referenced by:  weisoeq  7300  oiid  9477
  Copyright terms: Public domain W3C validator