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

Theorem ordiso2 6414
Description: Generalize ordiso 6415 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 4245 . . . . . 6 (Ord 𝐴𝐴 ⊆ On)
213ad2ant2 937 . . . . 5 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 ⊆ On)
32sseld 2971 . . . 4 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴𝑥 ∈ On))
4 eleq1 2116 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
5 fveq2 5205 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
6 id 19 . . . . . . . . 9 (𝑥 = 𝑦𝑥 = 𝑦)
75, 6eqeq12d 2070 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑦) = 𝑦))
84, 7imbi12d 227 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐴 → (𝐹𝑥) = 𝑥) ↔ (𝑦𝐴 → (𝐹𝑦) = 𝑦)))
98imbi2d 223 . . . . . 6 (𝑥 = 𝑦 → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦))))
10 r19.21v 2413 . . . . . . 7 (∀𝑦𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)))
11 ordelss 4143 . . . . . . . . . . . . . . . 16 ((Ord 𝐴𝑥𝐴) → 𝑥𝐴)
12113ad2antl2 1078 . . . . . . . . . . . . . . 15 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → 𝑥𝐴)
1312sselda 2972 . . . . . . . . . . . . . 14 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) ∧ 𝑦𝑥) → 𝑦𝐴)
14 pm5.5 235 . . . . . . . . . . . . . 14 (𝑦𝐴 → ((𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ (𝐹𝑦) = 𝑦))
1513, 14syl 14 . . . . . . . . . . . . 13 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) ∧ 𝑦𝑥) → ((𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ (𝐹𝑦) = 𝑦))
1615ralbidva 2339 . . . . . . . . . . . 12 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ ∀𝑦𝑥 (𝐹𝑦) = 𝑦))
17 isof1o 5474 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴1-1-onto𝐵)
18173ad2ant1 936 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴1-1-onto𝐵)
1918ad2antrr 465 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐴1-1-onto𝐵)
20 simpll3 956 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → Ord 𝐵)
21 simpr 107 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧 ∈ (𝐹𝑥))
22 f1of 5153 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2317, 22syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴𝐵)
24233ad2ant1 936 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴𝐵)
2524ad2antrr 465 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐴𝐵)
26 simplrl 495 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑥𝐴)
2725, 26ffvelrnd 5330 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑥) ∈ 𝐵)
2821, 27jca 294 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝑧 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝐵))
29 ordtr1 4152 . . . . . . . . . . . . . . . . . . 19 (Ord 𝐵 → ((𝑧 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝐵) → 𝑧𝐵))
3020, 28, 29sylc 60 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧𝐵)
31 f1ocnvfv2 5445 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴1-1-onto𝐵𝑧𝐵) → (𝐹‘(𝐹𝑧)) = 𝑧)
3219, 30, 31syl2anc 397 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) = 𝑧)
3332, 21eqeltrd 2130 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥))
34 simpll1 954 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹 Isom E , E (𝐴, 𝐵))
35 f1ocnv 5166 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
36 f1of 5153 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐵1-1-onto𝐴𝐹:𝐵𝐴)
3719, 35, 363syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐵𝐴)
3837, 30ffvelrnd 5330 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝐴)
39 isorel 5475 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ ((𝐹𝑧) ∈ 𝐴𝑥𝐴)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹‘(𝐹𝑧)) E (𝐹𝑥)))
4034, 38, 26, 39syl12anc 1144 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹‘(𝐹𝑧)) E (𝐹𝑥)))
41 vex 2577 . . . . . . . . . . . . . . . . . . . . . 22 𝑥 ∈ V
4241epelc 4055 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑧) E 𝑥 ↔ (𝐹𝑧) ∈ 𝑥)
4342a1i 9 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹𝑧) ∈ 𝑥))
44 f1ofn 5154 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
4517, 44syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
46 funfvex 5219 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Fun 𝐹𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ V)
4746funfni 5026 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 Fn 𝐴𝑥𝐴) → (𝐹𝑥) ∈ V)
4845, 47sylan 271 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑥𝐴) → (𝐹𝑥) ∈ V)
4934, 26, 48syl2anc 397 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑥) ∈ V)
50 epelg 4054 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑥) ∈ V → ((𝐹‘(𝐹𝑧)) E (𝐹𝑥) ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥)))
5149, 50syl 14 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹‘(𝐹𝑧)) E (𝐹𝑥) ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥)))
5240, 43, 513bitr3d 211 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) ∈ 𝑥 ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥)))
5333, 52mpbird 160 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝑥)
54 simplrr 496 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ∀𝑦𝑥 (𝐹𝑦) = 𝑦)
55 fveq2 5205 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐹𝑧) → (𝐹𝑦) = (𝐹‘(𝐹𝑧)))
56 id 19 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐹𝑧) → 𝑦 = (𝐹𝑧))
5755, 56eqeq12d 2070 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐹𝑧) → ((𝐹𝑦) = 𝑦 ↔ (𝐹‘(𝐹𝑧)) = (𝐹𝑧)))
5857rspcv 2669 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑧) ∈ 𝑥 → (∀𝑦𝑥 (𝐹𝑦) = 𝑦 → (𝐹‘(𝐹𝑧)) = (𝐹𝑧)))
5953, 54, 58sylc 60 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) = (𝐹𝑧))
6032, 59eqtr3d 2090 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧 = (𝐹𝑧))
6160, 53eqeltrd 2130 . . . . . . . . . . . . . . 15 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧𝑥)
62 simprr 492 . . . . . . . . . . . . . . . . 17 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → ∀𝑦𝑥 (𝐹𝑦) = 𝑦)
63 fveq2 5205 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹𝑧))
64 id 19 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧𝑦 = 𝑧)
6563, 64eqeq12d 2070 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((𝐹𝑦) = 𝑦 ↔ (𝐹𝑧) = 𝑧))
6665rspccva 2672 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝑥 (𝐹𝑦) = 𝑦𝑧𝑥) → (𝐹𝑧) = 𝑧)
6762, 66sylan 271 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) = 𝑧)
68 epel 4056 . . . . . . . . . . . . . . . . . . . 20 (𝑧 E 𝑥𝑧𝑥)
6968biimpri 128 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥𝑧 E 𝑥)
7069adantl 266 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧 E 𝑥)
71 simpll1 954 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
72 simpl2 919 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → Ord 𝐴)
73 simprl 491 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → 𝑥𝐴)
7472, 73, 11syl2anc 397 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → 𝑥𝐴)
7574sselda 2972 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧𝐴)
76 simplrl 495 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑥𝐴)
77 isorel 5475 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑧𝐴𝑥𝐴)) → (𝑧 E 𝑥 ↔ (𝐹𝑧) E (𝐹𝑥)))
7871, 75, 76, 77syl12anc 1144 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝑧 E 𝑥 ↔ (𝐹𝑧) E (𝐹𝑥)))
7970, 78mpbid 139 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) E (𝐹𝑥))
8071, 76, 48syl2anc 397 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑥) ∈ V)
81 epelg 4054 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥) ∈ V → ((𝐹𝑧) E (𝐹𝑥) ↔ (𝐹𝑧) ∈ (𝐹𝑥)))
8280, 81syl 14 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → ((𝐹𝑧) E (𝐹𝑥) ↔ (𝐹𝑧) ∈ (𝐹𝑥)))
8379, 82mpbid 139 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) ∈ (𝐹𝑥))
8467, 83eqeltrrd 2131 . . . . . . . . . . . . . . 15 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧 ∈ (𝐹𝑥))
8561, 84impbida 538 . . . . . . . . . . . . . 14 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → (𝑧 ∈ (𝐹𝑥) ↔ 𝑧𝑥))
8685eqrdv 2054 . . . . . . . . . . . . 13 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → (𝐹𝑥) = 𝑥)
8786expr 361 . . . . . . . . . . . 12 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝐹𝑦) = 𝑦 → (𝐹𝑥) = 𝑥))
8816, 87sylbid 143 . . . . . . . . . . 11 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝐹𝑥) = 𝑥))
8988ex 112 . . . . . . . . . 10 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝐹𝑥) = 𝑥)))
9089com23 76 . . . . . . . . 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 145 . . . . . 6 (𝑥 ∈ On → (∀𝑦𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))))
949, 93tfis2 4335 . . . . 5 (𝑥 ∈ On → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
9594com3l 79 . . . 4 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝑥 ∈ On → (𝐹𝑥) = 𝑥)))
963, 95mpdd 40 . . 3 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))
9796ralrimiv 2408 . 2 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑥𝐴 (𝐹𝑥) = 𝑥)
98 fveq2 5205 . . . . . . . . 9 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
99 id 19 . . . . . . . . 9 (𝑥 = 𝑧𝑥 = 𝑧)
10098, 99eqeq12d 2070 . . . . . . . 8 (𝑥 = 𝑧 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑧) = 𝑧))
101100rspccva 2672 . . . . . . 7 ((∀𝑥𝐴 (𝐹𝑥) = 𝑥𝑧𝐴) → (𝐹𝑧) = 𝑧)
102101adantll 453 . . . . . 6 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → (𝐹𝑧) = 𝑧)
10323ffvelrnda 5329 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
1041033ad2antl1 1077 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
105104adantlr 454 . . . . . 6 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
106102, 105eqeltrrd 2131 . . . . 5 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → 𝑧𝐵)
107106ex 112 . . . 4 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐴𝑧𝐵))
108 simpl1 918 . . . . . . . 8 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
109 f1ofo 5160 . . . . . . . . 9 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
110 forn 5136 . . . . . . . . 9 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
11117, 109, 1103syl 17 . . . . . . . 8 (𝐹 Isom E , E (𝐴, 𝐵) → ran 𝐹 = 𝐵)
112108, 111syl 14 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → ran 𝐹 = 𝐵)
113112eleq2d 2123 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹𝑧𝐵))
114453ad2ant1 936 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹 Fn 𝐴)
115114adantr 265 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐹 Fn 𝐴)
116 fvelrnb 5248 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
117115, 116syl 14 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
118113, 117bitr3d 183 . . . . 5 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐵 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
119 fveq2 5205 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
120 id 19 . . . . . . . . . . . 12 (𝑥 = 𝑤𝑥 = 𝑤)
121119, 120eqeq12d 2070 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑤) = 𝑤))
122121rspcv 2669 . . . . . . . . . 10 (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝐹𝑤) = 𝑤))
123122a1i 9 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝐹𝑤) = 𝑤)))
124 simpr 107 . . . . . . . . . . . . 13 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑧)
125 simpl 106 . . . . . . . . . . . . 13 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑤)
126124, 125eqtr3d 2090 . . . . . . . . . . . 12 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → 𝑧 = 𝑤)
127126adantl 266 . . . . . . . . . . 11 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑧 = 𝑤)
128 simplr 490 . . . . . . . . . . 11 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑤𝐴)
129127, 128eqeltrd 2130 . . . . . . . . . 10 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑧𝐴)
130129exp43 358 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → ((𝐹𝑤) = 𝑤 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
131123, 130syldd 65 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
132131com23 76 . . . . . . 7 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝑤𝐴 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
133132imp 119 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑤𝐴 → ((𝐹𝑤) = 𝑧𝑧𝐴)))
134133rexlimdv 2449 . . . . 5 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (∃𝑤𝐴 (𝐹𝑤) = 𝑧𝑧𝐴))
135118, 134sylbid 143 . . . 4 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐵𝑧𝐴))
136107, 135impbid 124 . . 3 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐴𝑧𝐵))
137136eqrdv 2054 . 2 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐴 = 𝐵)
13897, 137mpdan 406 1 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102  w3a 896   = wceq 1259  wcel 1409  wral 2323  wrex 2324  Vcvv 2574  wss 2944   class class class wbr 3791   E cep 4051  Ord word 4126  Oncon0 4127  ccnv 4371  ran crn 4373   Fn wfn 4924  wf 4925  ontowfo 4927  1-1-ontowf1o 4928  cfv 4929   Isom wiso 4930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-setind 4289
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-rab 2332  df-v 2576  df-sbc 2787  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-opab 3846  df-mpt 3847  df-tr 3882  df-eprel 4053  df-id 4057  df-iord 4130  df-on 4132  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937  df-isom 4938
This theorem is referenced by:  ordiso  6415
  Copyright terms: Public domain W3C validator