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

Theorem weniso 7354
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 4385 . . . . . 6 ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ ↔ ∃𝑎𝐴 ¬ (𝐹𝑎) = 𝑎)
2 rexnal 3099 . . . . . 6 (∃𝑎𝐴 ¬ (𝐹𝑎) = 𝑎 ↔ ¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
31, 2bitri 275 . . . . 5 ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ ↔ ¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
4 simpl1 1190 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → 𝑅 We 𝐴)
5 simpl2 1191 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → 𝑅 Se 𝐴)
6 ssrab2 4077 . . . . . . . . . 10 {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴
76a1i 11 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴)
8 simpr 484 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅)
9 wereu2 5673 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴 ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅)) → ∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
104, 5, 7, 8, 9syl22anc 836 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → ∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
11 reurex 3379 . . . . . . . 8 (∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
1210, 11syl 17 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
1312ex 412 . . . . . 6 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏))
14 fveq2 6891 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
15 id 22 . . . . . . . . . . 11 (𝑎 = 𝑏𝑎 = 𝑏)
1614, 15eqeq12d 2747 . . . . . . . . . 10 (𝑎 = 𝑏 → ((𝐹𝑎) = 𝑎 ↔ (𝐹𝑏) = 𝑏))
1716notbid 318 . . . . . . . . 9 (𝑎 = 𝑏 → (¬ (𝐹𝑎) = 𝑎 ↔ ¬ (𝐹𝑏) = 𝑏))
1817elrab 3683 . . . . . . . 8 (𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ↔ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏))
19 fveq2 6891 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
20 id 22 . . . . . . . . . . . . . 14 (𝑎 = 𝑐𝑎 = 𝑐)
2119, 20eqeq12d 2747 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → ((𝐹𝑎) = 𝑎 ↔ (𝐹𝑐) = 𝑐))
2221notbid 318 . . . . . . . . . . . 12 (𝑎 = 𝑐 → (¬ (𝐹𝑎) = 𝑎 ↔ ¬ (𝐹𝑐) = 𝑐))
2322ralrab 3689 . . . . . . . . . . 11 (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐𝐴 (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
24 con34b 316 . . . . . . . . . . . . 13 ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
2524bicomi 223 . . . . . . . . . . . 12 ((¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
2625ralbii 3092 . . . . . . . . . . 11 (∀𝑐𝐴 (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ ∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
2723, 26bitri 275 . . . . . . . . . 10 (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
28 simpl3 1192 . . . . . . . . . . . . . . . . . 18 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴))
29 isof1o 7323 . . . . . . . . . . . . . . . . . 18 (𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) → 𝐹:𝐴1-1-onto𝐴)
3028, 29syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴1-1-onto𝐴)
31 f1of 6833 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴𝐴)
3230, 31syl 17 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴𝐴)
33 simprl 768 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑏𝐴)
3432, 33ffvelcdmd 7087 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹𝑏) ∈ 𝐴)
35 breq1 5151 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → (𝑐𝑅𝑏 ↔ (𝐹𝑏)𝑅𝑏))
36 fveq2 6891 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝐹𝑏) → (𝐹𝑐) = (𝐹‘(𝐹𝑏)))
37 id 22 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝐹𝑏) → 𝑐 = (𝐹𝑏))
3836, 37eqeq12d 2747 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → ((𝐹𝑐) = 𝑐 ↔ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
3935, 38imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4039rspcv 3608 . . . . . . . . . . . . . . 15 ((𝐹𝑏) ∈ 𝐴 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4134, 40syl 17 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4241com23 86 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4342imp 406 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
44 f1of1 6832 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴1-1𝐴)
4530, 44syl 17 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴1-1𝐴)
46 f1fveq 7264 . . . . . . . . . . . . . . 15 ((𝐹:𝐴1-1𝐴 ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) ↔ (𝐹𝑏) = 𝑏))
4745, 34, 33, 46syl12anc 834 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) ↔ (𝐹𝑏) = 𝑏))
48 pm2.21 123 . . . . . . . . . . . . . . 15 (¬ (𝐹𝑏) = 𝑏 → ((𝐹𝑏) = 𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
4948ad2antll 726 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏) = 𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5047, 49sylbid 239 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5150adantr 480 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5243, 51syld 47 . . . . . . . . . . 11 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
53 f1ocnv 6845 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴1-1-onto𝐴)
54 f1of 6833 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴𝐴)
5530, 53, 543syl 18 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴𝐴)
5655, 33ffvelcdmd 7087 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹𝑏) ∈ 𝐴)
5756adantr 480 . . . . . . . . . . . . 13 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (𝐹𝑏) ∈ 𝐴)
58 isorel 7326 . . . . . . . . . . . . . . . 16 ((𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹𝑏)𝑅𝑏 ↔ (𝐹‘(𝐹𝑏))𝑅(𝐹𝑏)))
5928, 56, 33, 58syl12anc 834 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏 ↔ (𝐹‘(𝐹𝑏))𝑅(𝐹𝑏)))
60 f1ocnvfv2 7278 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐴1-1-onto𝐴𝑏𝐴) → (𝐹‘(𝐹𝑏)) = 𝑏)
6130, 33, 60syl2anc 583 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹‘(𝐹𝑏)) = 𝑏)
6261breq1d 5158 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏))𝑅(𝐹𝑏) ↔ 𝑏𝑅(𝐹𝑏)))
6359, 62bitr2d 280 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝑏𝑅(𝐹𝑏) ↔ (𝐹𝑏)𝑅𝑏))
6463biimpa 476 . . . . . . . . . . . . 13 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (𝐹𝑏)𝑅𝑏)
65 breq1 5151 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → (𝑐𝑅𝑏 ↔ (𝐹𝑏)𝑅𝑏))
66 fveq2 6891 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → (𝐹𝑐) = (𝐹‘(𝐹𝑏)))
67 id 22 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → 𝑐 = (𝐹𝑏))
6866, 67eqeq12d 2747 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → ((𝐹𝑐) = 𝑐 ↔ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
6965, 68imbi12d 344 . . . . . . . . . . . . . . 15 (𝑐 = (𝐹𝑏) → ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7069rspcv 3608 . . . . . . . . . . . . . 14 ((𝐹𝑏) ∈ 𝐴 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7170com23 86 . . . . . . . . . . . . 13 ((𝐹𝑏) ∈ 𝐴 → ((𝐹𝑏)𝑅𝑏 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7257, 64, 71sylc 65 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
73 simplrr 775 . . . . . . . . . . . . . . 15 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → ¬ (𝐹𝑏) = 𝑏)
74 fveq2 6891 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹‘(𝐹𝑏)))
7574adantl 481 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹‘(𝐹𝑏)))
7661fveq2d 6895 . . . . . . . . . . . . . . . . 17 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹𝑏))
7776adantr 480 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹𝑏))
7861adantr 480 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹𝑏)) = 𝑏)
7975, 77, 783eqtr3d 2779 . . . . . . . . . . . . . . 15 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹𝑏) = 𝑏)
8073, 79, 48sylc 65 . . . . . . . . . . . . . 14 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
8180ex 412 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
8281adantr 480 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
8372, 82syld 47 . . . . . . . . . . 11 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
84 simprr 770 . . . . . . . . . . . 12 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ¬ (𝐹𝑏) = 𝑏)
85 simpl1 1190 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑅 We 𝐴)
86 weso 5667 . . . . . . . . . . . . . . 15 (𝑅 We 𝐴𝑅 Or 𝐴)
8785, 86syl 17 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑅 Or 𝐴)
88 sotrieq 5617 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴 ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹𝑏) = 𝑏 ↔ ¬ ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏))))
8987, 34, 33, 88syl12anc 834 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏) = 𝑏 ↔ ¬ ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏))))
9089con2bid 354 . . . . . . . . . . . 12 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏)) ↔ ¬ (𝐹𝑏) = 𝑏))
9184, 90mpbird 257 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏)))
9252, 83, 91mpjaodan 956 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9327, 92biimtrid 241 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9493ex 412 . . . . . . . 8 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ((𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏) → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)))
9518, 94biimtrid 241 . . . . . . 7 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)))
9695rexlimdv 3152 . . . . . 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 7173 . . . . . 6 (𝑎𝐴 → (( I ↾ 𝐴)‘𝑎) = 𝑎)
101100eqeq2d 2742 . . . . 5 (𝑎𝐴 → ((𝐹𝑎) = (( I ↾ 𝐴)‘𝑎) ↔ (𝐹𝑎) = 𝑎))
102101biimprd 247 . . . 4 (𝑎𝐴 → ((𝐹𝑎) = 𝑎 → (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
103102ralimia 3079 . . 3 (∀𝑎𝐴 (𝐹𝑎) = 𝑎 → ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎))
10499, 103syl 17 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎))
105293ad2ant3 1134 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹:𝐴1-1-onto𝐴)
106 f1ofn 6834 . . . 4 (𝐹:𝐴1-1-onto𝐴𝐹 Fn 𝐴)
107105, 106syl 17 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 Fn 𝐴)
108 fnresi 6679 . . . 4 ( I ↾ 𝐴) Fn 𝐴
109108a1i 11 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ( I ↾ 𝐴) Fn 𝐴)
110 eqfnfv 7032 . . 3 ((𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
111107, 109, 110syl2anc 583 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
112104, 111mpbird 257 1 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844  w3a 1086   = wceq 1540  wcel 2105  wne 2939  wral 3060  wrex 3069  ∃!wreu 3373  {crab 3431  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 6538  wf 6539  1-1wf1 6540  1-1-ontowf1o 6542  cfv 6543   Isom wiso 6544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  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 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552
This theorem is referenced by:  weisoeq  7355  oiid  9542
  Copyright terms: Public domain W3C validator