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

Theorem ordiso2 8655
Description: Generalize ordiso 8656 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 7215 . . . . . 6 (Ord 𝐴𝐴 ⊆ On)
213ad2ant2 1157 . . . . 5 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 ⊆ On)
32sseld 3797 . . . 4 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴𝑥 ∈ On))
4 eleq1w 2868 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
5 fveq2 6404 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
6 id 22 . . . . . . . . 9 (𝑥 = 𝑦𝑥 = 𝑦)
75, 6eqeq12d 2821 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑦) = 𝑦))
84, 7imbi12d 335 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐴 → (𝐹𝑥) = 𝑥) ↔ (𝑦𝐴 → (𝐹𝑦) = 𝑦)))
98imbi2d 331 . . . . . 6 (𝑥 = 𝑦 → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦))))
10 r19.21v 3148 . . . . . . 7 (∀𝑦𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)))
11 ordelss 5952 . . . . . . . . . . . . . . . 16 ((Ord 𝐴𝑥𝐴) → 𝑥𝐴)
12113ad2antl2 1230 . . . . . . . . . . . . . . 15 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → 𝑥𝐴)
1312sselda 3798 . . . . . . . . . . . . . 14 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) ∧ 𝑦𝑥) → 𝑦𝐴)
14 pm5.5 352 . . . . . . . . . . . . . 14 (𝑦𝐴 → ((𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ (𝐹𝑦) = 𝑦))
1513, 14syl 17 . . . . . . . . . . . . 13 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) ∧ 𝑦𝑥) → ((𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ (𝐹𝑦) = 𝑦))
1615ralbidva 3173 . . . . . . . . . . . 12 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ ∀𝑦𝑥 (𝐹𝑦) = 𝑦))
17 isof1o 6793 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴1-1-onto𝐵)
18173ad2ant1 1156 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴1-1-onto𝐵)
1918ad2antrr 708 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐴1-1-onto𝐵)
20 simpll3 1266 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → Ord 𝐵)
21 simpr 473 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧 ∈ (𝐹𝑥))
22 f1of 6349 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2317, 22syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴𝐵)
24233ad2ant1 1156 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴𝐵)
2524ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐴𝐵)
26 simplrl 786 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑥𝐴)
27 ffvelrn 6575 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐴𝐵𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
2825, 26, 27syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑥) ∈ 𝐵)
2921, 28jca 503 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝑧 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝐵))
30 ordtr1 5979 . . . . . . . . . . . . . . . . . . 19 (Ord 𝐵 → ((𝑧 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝐵) → 𝑧𝐵))
3120, 29, 30sylc 65 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧𝐵)
32 f1ocnvfv2 6753 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴1-1-onto𝐵𝑧𝐵) → (𝐹‘(𝐹𝑧)) = 𝑧)
3319, 31, 32syl2anc 575 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) = 𝑧)
3433, 21eqeltrd 2885 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥))
35 simpll1 1262 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹 Isom E , E (𝐴, 𝐵))
36 f1ocnv 6361 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
37 f1of 6349 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐵1-1-onto𝐴𝐹:𝐵𝐴)
3819, 36, 373syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐵𝐴)
39 ffvelrn 6575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝐵𝐴𝑧𝐵) → (𝐹𝑧) ∈ 𝐴)
4038, 31, 39syl2anc 575 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝐴)
41 isorel 6796 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ ((𝐹𝑧) ∈ 𝐴𝑥𝐴)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹‘(𝐹𝑧)) E (𝐹𝑥)))
4235, 40, 26, 41syl12anc 856 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹‘(𝐹𝑧)) E (𝐹𝑥)))
43 epel 5227 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑧) E 𝑥 ↔ (𝐹𝑧) ∈ 𝑥)
44 fvex 6417 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑥) ∈ V
4544epeli 5226 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝐹𝑧)) E (𝐹𝑥) ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥))
4642, 43, 453bitr3g 304 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) ∈ 𝑥 ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥)))
4734, 46mpbird 248 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝑥)
48 simplrr 787 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ∀𝑦𝑥 (𝐹𝑦) = 𝑦)
49 fveq2 6404 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐹𝑧) → (𝐹𝑦) = (𝐹‘(𝐹𝑧)))
50 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐹𝑧) → 𝑦 = (𝐹𝑧))
5149, 50eqeq12d 2821 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐹𝑧) → ((𝐹𝑦) = 𝑦 ↔ (𝐹‘(𝐹𝑧)) = (𝐹𝑧)))
5251rspcv 3498 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑧) ∈ 𝑥 → (∀𝑦𝑥 (𝐹𝑦) = 𝑦 → (𝐹‘(𝐹𝑧)) = (𝐹𝑧)))
5347, 48, 52sylc 65 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) = (𝐹𝑧))
5433, 53eqtr3d 2842 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧 = (𝐹𝑧))
5554, 47eqeltrd 2885 . . . . . . . . . . . . . . 15 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧𝑥)
56 simprr 780 . . . . . . . . . . . . . . . . 17 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → ∀𝑦𝑥 (𝐹𝑦) = 𝑦)
57 fveq2 6404 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹𝑧))
58 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧𝑦 = 𝑧)
5957, 58eqeq12d 2821 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((𝐹𝑦) = 𝑦 ↔ (𝐹𝑧) = 𝑧))
6059rspccva 3501 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝑥 (𝐹𝑦) = 𝑦𝑧𝑥) → (𝐹𝑧) = 𝑧)
6156, 60sylan 571 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) = 𝑧)
62 epel 5227 . . . . . . . . . . . . . . . . . . . 20 (𝑧 E 𝑥𝑧𝑥)
6362biimpri 219 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥𝑧 E 𝑥)
6463adantl 469 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧 E 𝑥)
65 simpll1 1262 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
66 simpl2 1237 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → Ord 𝐴)
67 simprl 778 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → 𝑥𝐴)
6866, 67, 11syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → 𝑥𝐴)
6968sselda 3798 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧𝐴)
70 simplrl 786 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑥𝐴)
71 isorel 6796 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑧𝐴𝑥𝐴)) → (𝑧 E 𝑥 ↔ (𝐹𝑧) E (𝐹𝑥)))
7265, 69, 70, 71syl12anc 856 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝑧 E 𝑥 ↔ (𝐹𝑧) E (𝐹𝑥)))
7364, 72mpbid 223 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) E (𝐹𝑥))
7444epeli 5226 . . . . . . . . . . . . . . . . 17 ((𝐹𝑧) E (𝐹𝑥) ↔ (𝐹𝑧) ∈ (𝐹𝑥))
7573, 74sylib 209 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) ∈ (𝐹𝑥))
7661, 75eqeltrrd 2886 . . . . . . . . . . . . . . 15 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧 ∈ (𝐹𝑥))
7755, 76impbida 826 . . . . . . . . . . . . . 14 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → (𝑧 ∈ (𝐹𝑥) ↔ 𝑧𝑥))
7877eqrdv 2804 . . . . . . . . . . . . 13 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → (𝐹𝑥) = 𝑥)
7978expr 446 . . . . . . . . . . . 12 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝐹𝑦) = 𝑦 → (𝐹𝑥) = 𝑥))
8016, 79sylbid 231 . . . . . . . . . . 11 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝐹𝑥) = 𝑥))
8180ex 399 . . . . . . . . . 10 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝐹𝑥) = 𝑥)))
8281com23 86 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
8382a2i 14 . . . . . . . 8 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
8483a1i 11 . . . . . . 7 (𝑥 ∈ On → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))))
8510, 84syl5bi 233 . . . . . 6 (𝑥 ∈ On → (∀𝑦𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))))
869, 85tfis2 7282 . . . . 5 (𝑥 ∈ On → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
8786com3l 89 . . . 4 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝑥 ∈ On → (𝐹𝑥) = 𝑥)))
883, 87mpdd 43 . . 3 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))
8988ralrimiv 3153 . 2 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑥𝐴 (𝐹𝑥) = 𝑥)
90 fveq2 6404 . . . . . . . . 9 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
91 id 22 . . . . . . . . 9 (𝑥 = 𝑧𝑥 = 𝑧)
9290, 91eqeq12d 2821 . . . . . . . 8 (𝑥 = 𝑧 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑧) = 𝑧))
9392rspccva 3501 . . . . . . 7 ((∀𝑥𝐴 (𝐹𝑥) = 𝑥𝑧𝐴) → (𝐹𝑧) = 𝑧)
9493adantll 696 . . . . . 6 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → (𝐹𝑧) = 𝑧)
95 ffvelrn 6575 . . . . . . . . 9 ((𝐹:𝐴𝐵𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
9623, 95sylan 571 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
97963ad2antl1 1229 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
9897adantlr 697 . . . . . 6 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
9994, 98eqeltrrd 2886 . . . . 5 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → 𝑧𝐵)
10099ex 399 . . . 4 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐴𝑧𝐵))
101 simpl1 1235 . . . . . . . 8 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
102 f1ofo 6356 . . . . . . . . 9 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
103 forn 6330 . . . . . . . . 9 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
10417, 102, 1033syl 18 . . . . . . . 8 (𝐹 Isom E , E (𝐴, 𝐵) → ran 𝐹 = 𝐵)
105101, 104syl 17 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → ran 𝐹 = 𝐵)
106105eleq2d 2871 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹𝑧𝐵))
107 f1ofn 6350 . . . . . . . . . 10 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
10817, 107syl 17 . . . . . . . . 9 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
1091083ad2ant1 1156 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹 Fn 𝐴)
110109adantr 468 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐹 Fn 𝐴)
111 fvelrnb 6460 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
112110, 111syl 17 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
113106, 112bitr3d 272 . . . . 5 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐵 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
114 fveq2 6404 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
115 id 22 . . . . . . . . . . . 12 (𝑥 = 𝑤𝑥 = 𝑤)
116114, 115eqeq12d 2821 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑤) = 𝑤))
117116rspcv 3498 . . . . . . . . . 10 (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝐹𝑤) = 𝑤))
118117a1i 11 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝐹𝑤) = 𝑤)))
119 simpr 473 . . . . . . . . . . . . 13 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑧)
120 simpl 470 . . . . . . . . . . . . 13 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑤)
121119, 120eqtr3d 2842 . . . . . . . . . . . 12 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → 𝑧 = 𝑤)
122121adantl 469 . . . . . . . . . . 11 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑧 = 𝑤)
123 simplr 776 . . . . . . . . . . 11 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑤𝐴)
124122, 123eqeltrd 2885 . . . . . . . . . 10 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑧𝐴)
125124exp43 425 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → ((𝐹𝑤) = 𝑤 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
126118, 125syldd 72 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
127126com23 86 . . . . . . 7 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝑤𝐴 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
128127imp 395 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑤𝐴 → ((𝐹𝑤) = 𝑧𝑧𝐴)))
129128rexlimdv 3218 . . . . 5 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (∃𝑤𝐴 (𝐹𝑤) = 𝑧𝑧𝐴))
130113, 129sylbid 231 . . . 4 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐵𝑧𝐴))
131100, 130impbid 203 . . 3 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐴𝑧𝐵))
132131eqrdv 2804 . 2 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐴 = 𝐵)
13389, 132mpdan 670 1 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wral 3096  wrex 3097  wss 3769   class class class wbr 4844   E cep 5223  ccnv 5310  ran crn 5312  Ord word 5935  Oncon0 5936   Fn wfn 6092  wf 6093  ontowfo 6095  1-1-ontowf1o 6096  cfv 6097   Isom wiso 6098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-ord 5939  df-on 5940  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106
This theorem is referenced by:  ordiso  8656  oieu  8679  oiid  8681
  Copyright terms: Public domain W3C validator