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

Theorem ordiso2 9512
Description: Generalize ordiso 9513 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 7772 . . . . . 6 (Ord 𝐴𝐴 ⊆ On)
213ad2ant2 1132 . . . . 5 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 ⊆ On)
32sseld 3980 . . . 4 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴𝑥 ∈ On))
4 eleq1w 2814 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
5 fveq2 6890 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
6 id 22 . . . . . . . . 9 (𝑥 = 𝑦𝑥 = 𝑦)
75, 6eqeq12d 2746 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑦) = 𝑦))
84, 7imbi12d 343 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐴 → (𝐹𝑥) = 𝑥) ↔ (𝑦𝐴 → (𝐹𝑦) = 𝑦)))
98imbi2d 339 . . . . . 6 (𝑥 = 𝑦 → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦))))
10 r19.21v 3177 . . . . . . 7 (∀𝑦𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)))
11 ordelss 6379 . . . . . . . . . . . . . . . 16 ((Ord 𝐴𝑥𝐴) → 𝑥𝐴)
12113ad2antl2 1184 . . . . . . . . . . . . . . 15 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → 𝑥𝐴)
1312sselda 3981 . . . . . . . . . . . . . 14 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) ∧ 𝑦𝑥) → 𝑦𝐴)
14 pm5.5 360 . . . . . . . . . . . . . 14 (𝑦𝐴 → ((𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ (𝐹𝑦) = 𝑦))
1513, 14syl 17 . . . . . . . . . . . . 13 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) ∧ 𝑦𝑥) → ((𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ (𝐹𝑦) = 𝑦))
1615ralbidva 3173 . . . . . . . . . . . 12 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ ∀𝑦𝑥 (𝐹𝑦) = 𝑦))
17 isof1o 7322 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴1-1-onto𝐵)
18173ad2ant1 1131 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴1-1-onto𝐵)
1918ad2antrr 722 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐴1-1-onto𝐵)
20 simpll3 1212 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → Ord 𝐵)
21 simpr 483 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧 ∈ (𝐹𝑥))
22 f1of 6832 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2317, 22syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴𝐵)
24233ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴𝐵)
2524ad2antrr 722 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐴𝐵)
26 simplrl 773 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑥𝐴)
2725, 26ffvelcdmd 7086 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑥) ∈ 𝐵)
2821, 27jca 510 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝑧 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝐵))
29 ordtr1 6406 . . . . . . . . . . . . . . . . . . 19 (Ord 𝐵 → ((𝑧 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝐵) → 𝑧𝐵))
3020, 28, 29sylc 65 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧𝐵)
31 f1ocnvfv2 7277 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴1-1-onto𝐵𝑧𝐵) → (𝐹‘(𝐹𝑧)) = 𝑧)
3219, 30, 31syl2anc 582 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) = 𝑧)
3332, 21eqeltrd 2831 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥))
34 simpll1 1210 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹 Isom E , E (𝐴, 𝐵))
35 f1ocnv 6844 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
36 f1of 6832 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐵1-1-onto𝐴𝐹:𝐵𝐴)
3719, 35, 363syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐵𝐴)
3837, 30ffvelcdmd 7086 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝐴)
39 isorel 7325 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ ((𝐹𝑧) ∈ 𝐴𝑥𝐴)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹‘(𝐹𝑧)) E (𝐹𝑥)))
4034, 38, 26, 39syl12anc 833 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹‘(𝐹𝑧)) E (𝐹𝑥)))
41 epel 5582 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑧) E 𝑥 ↔ (𝐹𝑧) ∈ 𝑥)
42 fvex 6903 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑥) ∈ V
4342epeli 5581 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝐹𝑧)) E (𝐹𝑥) ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥))
4440, 41, 433bitr3g 312 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) ∈ 𝑥 ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥)))
4533, 44mpbird 256 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝑥)
46 simplrr 774 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ∀𝑦𝑥 (𝐹𝑦) = 𝑦)
47 fveq2 6890 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐹𝑧) → (𝐹𝑦) = (𝐹‘(𝐹𝑧)))
48 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐹𝑧) → 𝑦 = (𝐹𝑧))
4947, 48eqeq12d 2746 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐹𝑧) → ((𝐹𝑦) = 𝑦 ↔ (𝐹‘(𝐹𝑧)) = (𝐹𝑧)))
5049rspcv 3607 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑧) ∈ 𝑥 → (∀𝑦𝑥 (𝐹𝑦) = 𝑦 → (𝐹‘(𝐹𝑧)) = (𝐹𝑧)))
5145, 46, 50sylc 65 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) = (𝐹𝑧))
5232, 51eqtr3d 2772 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧 = (𝐹𝑧))
5352, 45eqeltrd 2831 . . . . . . . . . . . . . . 15 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧𝑥)
54 simprr 769 . . . . . . . . . . . . . . . . 17 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → ∀𝑦𝑥 (𝐹𝑦) = 𝑦)
55 fveq2 6890 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹𝑧))
56 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧𝑦 = 𝑧)
5755, 56eqeq12d 2746 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((𝐹𝑦) = 𝑦 ↔ (𝐹𝑧) = 𝑧))
5857rspccva 3610 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝑥 (𝐹𝑦) = 𝑦𝑧𝑥) → (𝐹𝑧) = 𝑧)
5954, 58sylan 578 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) = 𝑧)
60 epel 5582 . . . . . . . . . . . . . . . . . . . 20 (𝑧 E 𝑥𝑧𝑥)
6160biimpri 227 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥𝑧 E 𝑥)
6261adantl 480 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧 E 𝑥)
63 simpll1 1210 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
64 simpl2 1190 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → Ord 𝐴)
65 simprl 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → 𝑥𝐴)
6664, 65, 11syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → 𝑥𝐴)
6766sselda 3981 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧𝐴)
68 simplrl 773 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑥𝐴)
69 isorel 7325 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑧𝐴𝑥𝐴)) → (𝑧 E 𝑥 ↔ (𝐹𝑧) E (𝐹𝑥)))
7063, 67, 68, 69syl12anc 833 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝑧 E 𝑥 ↔ (𝐹𝑧) E (𝐹𝑥)))
7162, 70mpbid 231 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) E (𝐹𝑥))
7242epeli 5581 . . . . . . . . . . . . . . . . 17 ((𝐹𝑧) E (𝐹𝑥) ↔ (𝐹𝑧) ∈ (𝐹𝑥))
7371, 72sylib 217 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) ∈ (𝐹𝑥))
7459, 73eqeltrrd 2832 . . . . . . . . . . . . . . 15 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧 ∈ (𝐹𝑥))
7553, 74impbida 797 . . . . . . . . . . . . . 14 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → (𝑧 ∈ (𝐹𝑥) ↔ 𝑧𝑥))
7675eqrdv 2728 . . . . . . . . . . . . 13 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → (𝐹𝑥) = 𝑥)
7776expr 455 . . . . . . . . . . . 12 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝐹𝑦) = 𝑦 → (𝐹𝑥) = 𝑥))
7816, 77sylbid 239 . . . . . . . . . . 11 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝐹𝑥) = 𝑥))
7978ex 411 . . . . . . . . . 10 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝐹𝑥) = 𝑥)))
8079com23 86 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
8180a2i 14 . . . . . . . 8 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
8281a1i 11 . . . . . . 7 (𝑥 ∈ On → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))))
8310, 82biimtrid 241 . . . . . 6 (𝑥 ∈ On → (∀𝑦𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))))
849, 83tfis2 7848 . . . . 5 (𝑥 ∈ On → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
8584com3l 89 . . . 4 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝑥 ∈ On → (𝐹𝑥) = 𝑥)))
863, 85mpdd 43 . . 3 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))
8786ralrimiv 3143 . 2 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑥𝐴 (𝐹𝑥) = 𝑥)
88 fveq2 6890 . . . . . . . . 9 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
89 id 22 . . . . . . . . 9 (𝑥 = 𝑧𝑥 = 𝑧)
9088, 89eqeq12d 2746 . . . . . . . 8 (𝑥 = 𝑧 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑧) = 𝑧))
9190rspccva 3610 . . . . . . 7 ((∀𝑥𝐴 (𝐹𝑥) = 𝑥𝑧𝐴) → (𝐹𝑧) = 𝑧)
9291adantll 710 . . . . . 6 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → (𝐹𝑧) = 𝑧)
9323ffvelcdmda 7085 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
94933ad2antl1 1183 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
9594adantlr 711 . . . . . 6 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
9692, 95eqeltrrd 2832 . . . . 5 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → 𝑧𝐵)
9796ex 411 . . . 4 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐴𝑧𝐵))
98 simpl1 1189 . . . . . . . 8 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
99 f1ofo 6839 . . . . . . . . 9 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
100 forn 6807 . . . . . . . . 9 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
10117, 99, 1003syl 18 . . . . . . . 8 (𝐹 Isom E , E (𝐴, 𝐵) → ran 𝐹 = 𝐵)
10298, 101syl 17 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → ran 𝐹 = 𝐵)
103102eleq2d 2817 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹𝑧𝐵))
104 f1ofn 6833 . . . . . . . . . 10 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
10517, 104syl 17 . . . . . . . . 9 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
1061053ad2ant1 1131 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹 Fn 𝐴)
107106adantr 479 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐹 Fn 𝐴)
108 fvelrnb 6951 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
109107, 108syl 17 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
110103, 109bitr3d 280 . . . . 5 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐵 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
111 fveq2 6890 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
112 id 22 . . . . . . . . . . . 12 (𝑥 = 𝑤𝑥 = 𝑤)
113111, 112eqeq12d 2746 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑤) = 𝑤))
114113rspcv 3607 . . . . . . . . . 10 (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝐹𝑤) = 𝑤))
115114a1i 11 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝐹𝑤) = 𝑤)))
116 simpr 483 . . . . . . . . . . . . 13 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑧)
117 simpl 481 . . . . . . . . . . . . 13 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑤)
118116, 117eqtr3d 2772 . . . . . . . . . . . 12 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → 𝑧 = 𝑤)
119118adantl 480 . . . . . . . . . . 11 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑧 = 𝑤)
120 simplr 765 . . . . . . . . . . 11 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑤𝐴)
121119, 120eqeltrd 2831 . . . . . . . . . 10 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑧𝐴)
122121exp43 435 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → ((𝐹𝑤) = 𝑤 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
123115, 122syldd 72 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
124123com23 86 . . . . . . 7 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝑤𝐴 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
125124imp 405 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑤𝐴 → ((𝐹𝑤) = 𝑧𝑧𝐴)))
126125rexlimdv 3151 . . . . 5 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (∃𝑤𝐴 (𝐹𝑤) = 𝑧𝑧𝐴))
127110, 126sylbid 239 . . . 4 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐵𝑧𝐴))
12897, 127impbid 211 . . 3 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐴𝑧𝐵))
129128eqrdv 2728 . 2 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐴 = 𝐵)
13087, 129mpdan 683 1 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1085   = wceq 1539  wcel 2104  wral 3059  wrex 3068  wss 3947   class class class wbr 5147   E cep 5578  ccnv 5674  ran crn 5676  Ord word 6362  Oncon0 6363   Fn wfn 6537  wf 6538  ontowfo 6540  1-1-ontowf1o 6541  cfv 6542   Isom wiso 6543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551
This theorem is referenced by:  ordiso  9513  oieu  9536  oiid  9538
  Copyright terms: Public domain W3C validator