ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ordiso2 GIF version

Theorem ordiso2 6707
Description: Generalize ordiso 6708 to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015.)
Assertion
Ref Expression
ordiso2 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)

Proof of Theorem ordiso2
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordsson 4299 . . . . . 6 (Ord 𝐴𝐴 ⊆ On)
213ad2ant2 965 . . . . 5 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 ⊆ On)
32sseld 3022 . . . 4 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴𝑥 ∈ On))
4 eleq1 2150 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
5 fveq2 5289 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
6 id 19 . . . . . . . . 9 (𝑥 = 𝑦𝑥 = 𝑦)
75, 6eqeq12d 2102 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑦) = 𝑦))
84, 7imbi12d 232 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐴 → (𝐹𝑥) = 𝑥) ↔ (𝑦𝐴 → (𝐹𝑦) = 𝑦)))
98imbi2d 228 . . . . . 6 (𝑥 = 𝑦 → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦))))
10 r19.21v 2450 . . . . . . 7 (∀𝑦𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)))
11 ordelss 4197 . . . . . . . . . . . . . . . 16 ((Ord 𝐴𝑥𝐴) → 𝑥𝐴)
12113ad2antl2 1106 . . . . . . . . . . . . . . 15 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → 𝑥𝐴)
1312sselda 3023 . . . . . . . . . . . . . 14 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) ∧ 𝑦𝑥) → 𝑦𝐴)
14 pm5.5 240 . . . . . . . . . . . . . 14 (𝑦𝐴 → ((𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ (𝐹𝑦) = 𝑦))
1513, 14syl 14 . . . . . . . . . . . . 13 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) ∧ 𝑦𝑥) → ((𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ (𝐹𝑦) = 𝑦))
1615ralbidva 2376 . . . . . . . . . . . 12 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ ∀𝑦𝑥 (𝐹𝑦) = 𝑦))
17 isof1o 5568 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴1-1-onto𝐵)
18173ad2ant1 964 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴1-1-onto𝐵)
1918ad2antrr 472 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐴1-1-onto𝐵)
20 simpll3 984 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → Ord 𝐵)
21 simpr 108 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧 ∈ (𝐹𝑥))
22 f1of 5237 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2317, 22syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴𝐵)
24233ad2ant1 964 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴𝐵)
2524ad2antrr 472 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐴𝐵)
26 simplrl 502 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑥𝐴)
2725, 26ffvelrnd 5419 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑥) ∈ 𝐵)
2821, 27jca 300 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝑧 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝐵))
29 ordtr1 4206 . . . . . . . . . . . . . . . . . . 19 (Ord 𝐵 → ((𝑧 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝐵) → 𝑧𝐵))
3020, 28, 29sylc 61 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧𝐵)
31 f1ocnvfv2 5539 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴1-1-onto𝐵𝑧𝐵) → (𝐹‘(𝐹𝑧)) = 𝑧)
3219, 30, 31syl2anc 403 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) = 𝑧)
3332, 21eqeltrd 2164 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥))
34 simpll1 982 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹 Isom E , E (𝐴, 𝐵))
35 f1ocnv 5250 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
36 f1of 5237 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐵1-1-onto𝐴𝐹:𝐵𝐴)
3719, 35, 363syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐵𝐴)
3837, 30ffvelrnd 5419 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝐴)
39 isorel 5569 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ ((𝐹𝑧) ∈ 𝐴𝑥𝐴)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹‘(𝐹𝑧)) E (𝐹𝑥)))
4034, 38, 26, 39syl12anc 1172 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹‘(𝐹𝑧)) E (𝐹𝑥)))
41 vex 2622 . . . . . . . . . . . . . . . . . . . . . 22 𝑥 ∈ V
4241epelc 4109 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑧) E 𝑥 ↔ (𝐹𝑧) ∈ 𝑥)
4342a1i 9 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹𝑧) ∈ 𝑥))
44 f1ofn 5238 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
4517, 44syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
46 funfvex 5306 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ V)
4746funfni 5100 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 Fn 𝐴𝑥𝐴) → (𝐹𝑥) ∈ V)
4845, 47sylan 277 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ V)
4934, 26, 48syl2anc 403 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑥) ∈ V)
50 epelg 4108 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑥) ∈ V → ((𝐹‘(𝐹𝑧)) E (𝐹𝑥) ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥)))
5149, 50syl 14 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹‘(𝐹𝑧)) E (𝐹𝑥) ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥)))
5240, 43, 513bitr3d 216 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) ∈ 𝑥 ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥)))
5333, 52mpbird 165 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝑥)
54 simplrr 503 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ∀𝑦𝑥 (𝐹𝑦) = 𝑦)
55 fveq2 5289 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐹𝑧) → (𝐹𝑦) = (𝐹‘(𝐹𝑧)))
56 id 19 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐹𝑧) → 𝑦 = (𝐹𝑧))
5755, 56eqeq12d 2102 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐹𝑧) → ((𝐹𝑦) = 𝑦 ↔ (𝐹‘(𝐹𝑧)) = (𝐹𝑧)))
5857rspcv 2718 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑧) ∈ 𝑥 → (∀𝑦𝑥 (𝐹𝑦) = 𝑦 → (𝐹‘(𝐹𝑧)) = (𝐹𝑧)))
5953, 54, 58sylc 61 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) = (𝐹𝑧))
6032, 59eqtr3d 2122 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧 = (𝐹𝑧))
6160, 53eqeltrd 2164 . . . . . . . . . . . . . . 15 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧𝑥)
62 simprr 499 . . . . . . . . . . . . . . . . 17 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → ∀𝑦𝑥 (𝐹𝑦) = 𝑦)
63 fveq2 5289 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹𝑧))
64 id 19 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧𝑦 = 𝑧)
6563, 64eqeq12d 2102 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((𝐹𝑦) = 𝑦 ↔ (𝐹𝑧) = 𝑧))
6665rspccva 2721 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝑥 (𝐹𝑦) = 𝑦𝑧𝑥) → (𝐹𝑧) = 𝑧)
6762, 66sylan 277 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) = 𝑧)
68 epel 4110 . . . . . . . . . . . . . . . . . . . 20 (𝑧 E 𝑥𝑧𝑥)
6968biimpri 131 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥𝑧 E 𝑥)
7069adantl 271 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧 E 𝑥)
71 simpll1 982 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
72 simpl2 947 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → Ord 𝐴)
73 simprl 498 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → 𝑥𝐴)
7472, 73, 11syl2anc 403 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → 𝑥𝐴)
7574sselda 3023 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧𝐴)
76 simplrl 502 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑥𝐴)
77 isorel 5569 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑧𝐴𝑥𝐴)) → (𝑧 E 𝑥 ↔ (𝐹𝑧) E (𝐹𝑥)))
7871, 75, 76, 77syl12anc 1172 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝑧 E 𝑥 ↔ (𝐹𝑧) E (𝐹𝑥)))
7970, 78mpbid 145 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) E (𝐹𝑥))
8071, 76, 48syl2anc 403 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑥) ∈ V)
81 epelg 4108 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) ∈ V → ((𝐹𝑧) E (𝐹𝑥) ↔ (𝐹𝑧) ∈ (𝐹𝑥)))
8280, 81syl 14 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → ((𝐹𝑧) E (𝐹𝑥) ↔ (𝐹𝑧) ∈ (𝐹𝑥)))
8379, 82mpbid 145 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) ∈ (𝐹𝑥))
8467, 83eqeltrrd 2165 . . . . . . . . . . . . . . 15 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧 ∈ (𝐹𝑥))
8561, 84impbida 563 . . . . . . . . . . . . . 14 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → (𝑧 ∈ (𝐹𝑥) ↔ 𝑧𝑥))
8685eqrdv 2086 . . . . . . . . . . . . 13 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → (𝐹𝑥) = 𝑥)
8786expr 367 . . . . . . . . . . . 12 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝐹𝑦) = 𝑦 → (𝐹𝑥) = 𝑥))
8816, 87sylbid 148 . . . . . . . . . . 11 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝐹𝑥) = 𝑥))
8988ex 113 . . . . . . . . . 10 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝐹𝑥) = 𝑥)))
9089com23 77 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
9190a2i 11 . . . . . . . 8 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
9291a1i 9 . . . . . . 7 (𝑥 ∈ On → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))))
9310, 92syl5bi 150 . . . . . 6 (𝑥 ∈ On → (∀𝑦𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))))
949, 93tfis2 4390 . . . . 5 (𝑥 ∈ On → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
9594com3l 80 . . . 4 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝑥 ∈ On → (𝐹𝑥) = 𝑥)))
963, 95mpdd 40 . . 3 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))
9796ralrimiv 2445 . 2 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑥𝐴 (𝐹𝑥) = 𝑥)
98 fveq2 5289 . . . . . . . . 9 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
99 id 19 . . . . . . . . 9 (𝑥 = 𝑧𝑥 = 𝑧)
10098, 99eqeq12d 2102 . . . . . . . 8 (𝑥 = 𝑧 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑧) = 𝑧))
101100rspccva 2721 . . . . . . 7 ((∀𝑥𝐴 (𝐹𝑥) = 𝑥𝑧𝐴) → (𝐹𝑧) = 𝑧)
102101adantll 460 . . . . . 6 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → (𝐹𝑧) = 𝑧)
10323ffvelrnda 5418 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
1041033ad2antl1 1105 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
105104adantlr 461 . . . . . 6 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
106102, 105eqeltrrd 2165 . . . . 5 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → 𝑧𝐵)
107106ex 113 . . . 4 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐴𝑧𝐵))
108 simpl1 946 . . . . . . . 8 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
109 f1ofo 5244 . . . . . . . . 9 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
110 forn 5220 . . . . . . . . 9 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
11117, 109, 1103syl 17 . . . . . . . 8 (𝐹 Isom E , E (𝐴, 𝐵) → ran 𝐹 = 𝐵)
112108, 111syl 14 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → ran 𝐹 = 𝐵)
113112eleq2d 2157 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹𝑧𝐵))
114453ad2ant1 964 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹 Fn 𝐴)
115114adantr 270 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐹 Fn 𝐴)
116 fvelrnb 5336 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
117115, 116syl 14 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
118113, 117bitr3d 188 . . . . 5 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐵 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
119 fveq2 5289 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
120 id 19 . . . . . . . . . . . 12 (𝑥 = 𝑤𝑥 = 𝑤)
121119, 120eqeq12d 2102 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑤) = 𝑤))
122121rspcv 2718 . . . . . . . . . 10 (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝐹𝑤) = 𝑤))
123122a1i 9 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝐹𝑤) = 𝑤)))
124 simpr 108 . . . . . . . . . . . . 13 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑧)
125 simpl 107 . . . . . . . . . . . . 13 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑤)
126124, 125eqtr3d 2122 . . . . . . . . . . . 12 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → 𝑧 = 𝑤)
127126adantl 271 . . . . . . . . . . 11 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑧 = 𝑤)
128 simplr 497 . . . . . . . . . . 11 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑤𝐴)
129127, 128eqeltrd 2164 . . . . . . . . . 10 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑧𝐴)
130129exp43 364 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → ((𝐹𝑤) = 𝑤 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
131123, 130syldd 66 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
132131com23 77 . . . . . . 7 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝑤𝐴 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
133132imp 122 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑤𝐴 → ((𝐹𝑤) = 𝑧𝑧𝐴)))
134133rexlimdv 2488 . . . . 5 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (∃𝑤𝐴 (𝐹𝑤) = 𝑧𝑧𝐴))
135118, 134sylbid 148 . . . 4 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐵𝑧𝐴))
136107, 135impbid 127 . . 3 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐴𝑧𝐵))
137136eqrdv 2086 . 2 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐴 = 𝐵)
13897, 137mpdan 412 1 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 924   = wceq 1289  wcel 1438  wral 2359  wrex 2360  Vcvv 2619  wss 2997   class class class wbr 3837   E cep 4105  Ord word 4180  Oncon0 4181  ccnv 4427  ran crn 4429   Fn wfn 4997  wf 4998  ontowfo 5000  1-1-ontowf1o 5001  cfv 5002   Isom wiso 5003
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027  ax-setind 4343
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-sbc 2839  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-mpt 3893  df-tr 3929  df-eprel 4107  df-id 4111  df-iord 4184  df-on 4186  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009  df-fv 5010  df-isom 5011
This theorem is referenced by:  ordiso  6708
  Copyright terms: Public domain W3C validator