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

Theorem weniso 6504
 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 3912 . . . . . 6 ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ ↔ ∃𝑎𝐴 ¬ (𝐹𝑎) = 𝑎)
2 rexnal 2978 . . . . . 6 (∃𝑎𝐴 ¬ (𝐹𝑎) = 𝑎 ↔ ¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
31, 2bitri 263 . . . . 5 ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ ↔ ¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
4 simpl1 1057 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → 𝑅 We 𝐴)
5 simpl2 1058 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → 𝑅 Se 𝐴)
6 ssrab2 3650 . . . . . . . . . 10 {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴
76a1i 11 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴)
8 simpr 476 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅)
9 wereu2 5035 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ⊆ 𝐴 ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅)) → ∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
104, 5, 7, 8, 9syl22anc 1319 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → ∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
11 reurex 3137 . . . . . . . 8 (∃!𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
1210, 11syl 17 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅) → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏)
1312ex 449 . . . . . 6 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ → ∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏))
14 fveq2 6103 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
15 id 22 . . . . . . . . . . 11 (𝑎 = 𝑏𝑎 = 𝑏)
1614, 15eqeq12d 2625 . . . . . . . . . 10 (𝑎 = 𝑏 → ((𝐹𝑎) = 𝑎 ↔ (𝐹𝑏) = 𝑏))
1716notbid 307 . . . . . . . . 9 (𝑎 = 𝑏 → (¬ (𝐹𝑎) = 𝑎 ↔ ¬ (𝐹𝑏) = 𝑏))
1817elrab 3331 . . . . . . . 8 (𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ↔ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏))
19 fveq2 6103 . . . . . . . . . . . . . 14 (𝑎 = 𝑐 → (𝐹𝑎) = (𝐹𝑐))
20 id 22 . . . . . . . . . . . . . 14 (𝑎 = 𝑐𝑎 = 𝑐)
2119, 20eqeq12d 2625 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → ((𝐹𝑎) = 𝑎 ↔ (𝐹𝑐) = 𝑐))
2221notbid 307 . . . . . . . . . . . 12 (𝑎 = 𝑐 → (¬ (𝐹𝑎) = 𝑎 ↔ ¬ (𝐹𝑐) = 𝑐))
2322ralrab 3335 . . . . . . . . . . 11 (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐𝐴 (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
24 con34b 305 . . . . . . . . . . . . 13 ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏))
2524bicomi 213 . . . . . . . . . . . 12 ((¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
2625ralbii 2963 . . . . . . . . . . 11 (∀𝑐𝐴 (¬ (𝐹𝑐) = 𝑐 → ¬ 𝑐𝑅𝑏) ↔ ∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
2723, 26bitri 263 . . . . . . . . . 10 (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 ↔ ∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐))
28 simpl3 1059 . . . . . . . . . . . . . . . . . 18 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴))
29 isof1o 6473 . . . . . . . . . . . . . . . . . 18 (𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) → 𝐹:𝐴1-1-onto𝐴)
3028, 29syl 17 . . . . . . . . . . . . . . . . 17 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴1-1-onto𝐴)
31 f1of 6050 . . . . . . . . . . . . . . . . 17 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴𝐴)
3230, 31syl 17 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴𝐴)
33 simprl 790 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑏𝐴)
3432, 33ffvelrnd 6268 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹𝑏) ∈ 𝐴)
35 breq1 4586 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → (𝑐𝑅𝑏 ↔ (𝐹𝑏)𝑅𝑏))
36 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝐹𝑏) → (𝐹𝑐) = (𝐹‘(𝐹𝑏)))
37 id 22 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝐹𝑏) → 𝑐 = (𝐹𝑏))
3836, 37eqeq12d 2625 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → ((𝐹𝑐) = 𝑐 ↔ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
3935, 38imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4039rspcv 3278 . . . . . . . . . . . . . . 15 ((𝐹𝑏) ∈ 𝐴 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4134, 40syl 17 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4241com23 84 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
4342imp 444 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
44 f1of1 6049 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴1-1𝐴)
4530, 44syl 17 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴1-1𝐴)
46 f1fveq 6420 . . . . . . . . . . . . . . 15 ((𝐹:𝐴1-1𝐴 ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) ↔ (𝐹𝑏) = 𝑏))
4745, 34, 33, 46syl12anc 1316 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) ↔ (𝐹𝑏) = 𝑏))
48 pm2.21 119 . . . . . . . . . . . . . . 15 (¬ (𝐹𝑏) = 𝑏 → ((𝐹𝑏) = 𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
4948ad2antll 761 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏) = 𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5047, 49sylbid 229 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5150adantr 480 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
5243, 51syld 46 . . . . . . . . . . 11 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹𝑏)𝑅𝑏) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
53 f1ocnv 6062 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴1-1-onto𝐴)
54 f1of 6050 . . . . . . . . . . . . . . . 16 (𝐹:𝐴1-1-onto𝐴𝐹:𝐴𝐴)
5530, 53, 543syl 18 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝐹:𝐴𝐴)
5655, 33ffvelrnd 6268 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹𝑏) ∈ 𝐴)
5756adantr 480 . . . . . . . . . . . . 13 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (𝐹𝑏) ∈ 𝐴)
58 isorel 6476 . . . . . . . . . . . . . . . 16 ((𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴) ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹𝑏)𝑅𝑏 ↔ (𝐹‘(𝐹𝑏))𝑅(𝐹𝑏)))
5928, 56, 33, 58syl12anc 1316 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏 ↔ (𝐹‘(𝐹𝑏))𝑅(𝐹𝑏)))
60 f1ocnvfv2 6433 . . . . . . . . . . . . . . . . 17 ((𝐹:𝐴1-1-onto𝐴𝑏𝐴) → (𝐹‘(𝐹𝑏)) = 𝑏)
6130, 33, 60syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹‘(𝐹𝑏)) = 𝑏)
6261breq1d 4593 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏))𝑅(𝐹𝑏) ↔ 𝑏𝑅(𝐹𝑏)))
6359, 62bitr2d 268 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝑏𝑅(𝐹𝑏) ↔ (𝐹𝑏)𝑅𝑏))
6463biimpa 500 . . . . . . . . . . . . 13 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (𝐹𝑏)𝑅𝑏)
65 breq1 4586 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → (𝑐𝑅𝑏 ↔ (𝐹𝑏)𝑅𝑏))
66 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → (𝐹𝑐) = (𝐹‘(𝐹𝑏)))
67 id 22 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑏) → 𝑐 = (𝐹𝑏))
6866, 67eqeq12d 2625 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑏) → ((𝐹𝑐) = 𝑐 ↔ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
6965, 68imbi12d 333 . . . . . . . . . . . . . . 15 (𝑐 = (𝐹𝑏) → ((𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) ↔ ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7069rspcv 3278 . . . . . . . . . . . . . 14 ((𝐹𝑏) ∈ 𝐴 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ((𝐹𝑏)𝑅𝑏 → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7170com23 84 . . . . . . . . . . . . 13 ((𝐹𝑏) ∈ 𝐴 → ((𝐹𝑏)𝑅𝑏 → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏))))
7257, 64, 71sylc 63 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → (𝐹‘(𝐹𝑏)) = (𝐹𝑏)))
73 simplrr 797 . . . . . . . . . . . . . . 15 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → ¬ (𝐹𝑏) = 𝑏)
74 fveq2 6103 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹‘(𝐹𝑏)))
7574adantl 481 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹‘(𝐹𝑏)))
7661fveq2d 6107 . . . . . . . . . . . . . . . . 17 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹𝑏))
7776adantr 480 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹‘(𝐹𝑏))) = (𝐹𝑏))
7861adantr 480 . . . . . . . . . . . . . . . 16 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹‘(𝐹𝑏)) = 𝑏)
7975, 77, 783eqtr3d 2652 . . . . . . . . . . . . . . 15 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → (𝐹𝑏) = 𝑏)
8073, 79, 48sylc 63 . . . . . . . . . . . . . 14 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ (𝐹‘(𝐹𝑏)) = (𝐹𝑏)) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
8180ex 449 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
8281adantr 480 . . . . . . . . . . . 12 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → ((𝐹‘(𝐹𝑏)) = (𝐹𝑏) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
8372, 82syld 46 . . . . . . . . . . 11 ((((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) ∧ 𝑏𝑅(𝐹𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
84 simprr 792 . . . . . . . . . . . 12 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ¬ (𝐹𝑏) = 𝑏)
85 simpl1 1057 . . . . . . . . . . . . . . 15 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑅 We 𝐴)
86 weso 5029 . . . . . . . . . . . . . . 15 (𝑅 We 𝐴𝑅 Or 𝐴)
8785, 86syl 17 . . . . . . . . . . . . . 14 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → 𝑅 Or 𝐴)
88 sotrieq 4986 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴 ∧ ((𝐹𝑏) ∈ 𝐴𝑏𝐴)) → ((𝐹𝑏) = 𝑏 ↔ ¬ ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏))))
8987, 34, 33, 88syl12anc 1316 . . . . . . . . . . . . 13 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏) = 𝑏 ↔ ¬ ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏))))
9089con2bid 343 . . . . . . . . . . . 12 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏)) ↔ ¬ (𝐹𝑏) = 𝑏))
9184, 90mpbird 246 . . . . . . . . . . 11 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → ((𝐹𝑏)𝑅𝑏𝑏𝑅(𝐹𝑏)))
9252, 83, 91mpjaodan 823 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐𝐴 (𝑐𝑅𝑏 → (𝐹𝑐) = 𝑐) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9327, 92syl5bi 231 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) ∧ (𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏)) → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9493ex 449 . . . . . . . 8 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ((𝑏𝐴 ∧ ¬ (𝐹𝑏) = 𝑏) → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)))
9518, 94syl5bi 231 . . . . . . 7 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} → (∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)))
9695rexlimdv 3012 . . . . . 6 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (∃𝑏 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎}∀𝑐 ∈ {𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ¬ 𝑐𝑅𝑏 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9713, 96syld 46 . . . . 5 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ({𝑎𝐴 ∣ ¬ (𝐹𝑎) = 𝑎} ≠ ∅ → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
983, 97syl5bir 232 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (¬ ∀𝑎𝐴 (𝐹𝑎) = 𝑎 → ∀𝑎𝐴 (𝐹𝑎) = 𝑎))
9998pm2.18d 123 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎𝐴 (𝐹𝑎) = 𝑎)
100 fvresi 6344 . . . . . 6 (𝑎𝐴 → (( I ↾ 𝐴)‘𝑎) = 𝑎)
101100eqeq2d 2620 . . . . 5 (𝑎𝐴 → ((𝐹𝑎) = (( I ↾ 𝐴)‘𝑎) ↔ (𝐹𝑎) = 𝑎))
102101biimprd 237 . . . 4 (𝑎𝐴 → ((𝐹𝑎) = 𝑎 → (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
103102ralimia 2934 . . 3 (∀𝑎𝐴 (𝐹𝑎) = 𝑎 → ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎))
10499, 103syl 17 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎))
105293ad2ant3 1077 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹:𝐴1-1-onto𝐴)
106 f1ofn 6051 . . . 4 (𝐹:𝐴1-1-onto𝐴𝐹 Fn 𝐴)
107105, 106syl 17 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 Fn 𝐴)
108 fnresi 5922 . . . 4 ( I ↾ 𝐴) Fn 𝐴
109108a1i 11 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → ( I ↾ 𝐴) Fn 𝐴)
110 eqfnfv 6219 . . 3 ((𝐹 Fn 𝐴 ∧ ( I ↾ 𝐴) Fn 𝐴) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
111107, 109, 110syl2anc 691 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → (𝐹 = ( I ↾ 𝐴) ↔ ∀𝑎𝐴 (𝐹𝑎) = (( I ↾ 𝐴)‘𝑎)))
112104, 111mpbird 246 1 ((𝑅 We 𝐴𝑅 Se 𝐴𝐹 Isom 𝑅, 𝑅 (𝐴, 𝐴)) → 𝐹 = ( I ↾ 𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  {crab 2900   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   I cid 4948   Or wor 4958   Se wse 4995   We wwe 4996  ◡ccnv 5037   ↾ cres 5040   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813 This theorem is referenced by:  weisoeq  6505  oiid  8329
 Copyright terms: Public domain W3C validator