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

Theorem ordiso2 8371
Description: Generalize ordiso 8372 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 6943 . . . . . 6 (Ord 𝐴𝐴 ⊆ On)
213ad2ant2 1081 . . . . 5 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 ⊆ On)
32sseld 3586 . . . 4 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴𝑥 ∈ On))
4 eleq1 2686 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
5 fveq2 6153 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
6 id 22 . . . . . . . . 9 (𝑥 = 𝑦𝑥 = 𝑦)
75, 6eqeq12d 2636 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑦) = 𝑦))
84, 7imbi12d 334 . . . . . . 7 (𝑥 = 𝑦 → ((𝑥𝐴 → (𝐹𝑥) = 𝑥) ↔ (𝑦𝐴 → (𝐹𝑦) = 𝑦)))
98imbi2d 330 . . . . . 6 (𝑥 = 𝑦 → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦))))
10 r19.21v 2955 . . . . . . 7 (∀𝑦𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)))
11 ordelss 5703 . . . . . . . . . . . . . . . 16 ((Ord 𝐴𝑥𝐴) → 𝑥𝐴)
12113ad2antl2 1222 . . . . . . . . . . . . . . 15 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → 𝑥𝐴)
1312sselda 3587 . . . . . . . . . . . . . 14 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) ∧ 𝑦𝑥) → 𝑦𝐴)
14 pm5.5 351 . . . . . . . . . . . . . 14 (𝑦𝐴 → ((𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ (𝐹𝑦) = 𝑦))
1513, 14syl 17 . . . . . . . . . . . . 13 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) ∧ 𝑦𝑥) → ((𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ (𝐹𝑦) = 𝑦))
1615ralbidva 2980 . . . . . . . . . . . 12 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) ↔ ∀𝑦𝑥 (𝐹𝑦) = 𝑦))
17 isof1o 6533 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴1-1-onto𝐵)
18173ad2ant1 1080 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴1-1-onto𝐵)
1918ad2antrr 761 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐴1-1-onto𝐵)
20 simpll3 1100 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → Ord 𝐵)
21 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧 ∈ (𝐹𝑥))
22 f1of 6099 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2317, 22syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴𝐵)
24233ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴𝐵)
2524ad2antrr 761 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐴𝐵)
26 simplrl 799 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑥𝐴)
27 ffvelrn 6318 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:𝐴𝐵𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
2825, 26, 27syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑥) ∈ 𝐵)
2921, 28jca 554 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝑧 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝐵))
30 ordtr1 5731 . . . . . . . . . . . . . . . . . . 19 (Ord 𝐵 → ((𝑧 ∈ (𝐹𝑥) ∧ (𝐹𝑥) ∈ 𝐵) → 𝑧𝐵))
3120, 29, 30sylc 65 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧𝐵)
32 f1ocnvfv2 6493 . . . . . . . . . . . . . . . . . 18 ((𝐹:𝐴1-1-onto𝐵𝑧𝐵) → (𝐹‘(𝐹𝑧)) = 𝑧)
3319, 31, 32syl2anc 692 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) = 𝑧)
3433, 21eqeltrd 2698 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥))
35 simpll1 1098 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹 Isom E , E (𝐴, 𝐵))
36 f1ocnv 6111 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
37 f1of 6099 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝐵1-1-onto𝐴𝐹:𝐵𝐴)
3819, 36, 373syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝐹:𝐵𝐴)
39 ffvelrn 6318 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝐵𝐴𝑧𝐵) → (𝐹𝑧) ∈ 𝐴)
4038, 31, 39syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝐴)
41 isorel 6536 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ ((𝐹𝑧) ∈ 𝐴𝑥𝐴)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹‘(𝐹𝑧)) E (𝐹𝑥)))
4235, 40, 26, 41syl12anc 1321 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) E 𝑥 ↔ (𝐹‘(𝐹𝑧)) E (𝐹𝑥)))
43 vex 3192 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
4443epelc 4992 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑧) E 𝑥 ↔ (𝐹𝑧) ∈ 𝑥)
45 fvex 6163 . . . . . . . . . . . . . . . . . . . . 21 (𝐹𝑥) ∈ V
4645epelc 4992 . . . . . . . . . . . . . . . . . . . 20 ((𝐹‘(𝐹𝑧)) E (𝐹𝑥) ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥))
4742, 44, 463bitr3g 302 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ((𝐹𝑧) ∈ 𝑥 ↔ (𝐹‘(𝐹𝑧)) ∈ (𝐹𝑥)))
4834, 47mpbird 247 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹𝑧) ∈ 𝑥)
49 simplrr 800 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → ∀𝑦𝑥 (𝐹𝑦) = 𝑦)
50 fveq2 6153 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐹𝑧) → (𝐹𝑦) = (𝐹‘(𝐹𝑧)))
51 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝐹𝑧) → 𝑦 = (𝐹𝑧))
5250, 51eqeq12d 2636 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝐹𝑧) → ((𝐹𝑦) = 𝑦 ↔ (𝐹‘(𝐹𝑧)) = (𝐹𝑧)))
5352rspcv 3294 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑧) ∈ 𝑥 → (∀𝑦𝑥 (𝐹𝑦) = 𝑦 → (𝐹‘(𝐹𝑧)) = (𝐹𝑧)))
5448, 49, 53sylc 65 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → (𝐹‘(𝐹𝑧)) = (𝐹𝑧))
5533, 54eqtr3d 2657 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧 = (𝐹𝑧))
5655, 48eqeltrd 2698 . . . . . . . . . . . . . . 15 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹𝑥)) → 𝑧𝑥)
57 simprr 795 . . . . . . . . . . . . . . . . 17 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → ∀𝑦𝑥 (𝐹𝑦) = 𝑦)
58 fveq2 6153 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (𝐹𝑦) = (𝐹𝑧))
59 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧𝑦 = 𝑧)
6058, 59eqeq12d 2636 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((𝐹𝑦) = 𝑦 ↔ (𝐹𝑧) = 𝑧))
6160rspccva 3297 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝑥 (𝐹𝑦) = 𝑦𝑧𝑥) → (𝐹𝑧) = 𝑧)
6257, 61sylan 488 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) = 𝑧)
63 epel 4993 . . . . . . . . . . . . . . . . . . . 20 (𝑧 E 𝑥𝑧𝑥)
6463biimpri 218 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥𝑧 E 𝑥)
6564adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧 E 𝑥)
66 simpll1 1098 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
67 simpl2 1063 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → Ord 𝐴)
68 simprl 793 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → 𝑥𝐴)
6967, 68, 11syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → 𝑥𝐴)
7069sselda 3587 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧𝐴)
71 simplrl 799 . . . . . . . . . . . . . . . . . . 19 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑥𝐴)
72 isorel 6536 . . . . . . . . . . . . . . . . . . 19 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑧𝐴𝑥𝐴)) → (𝑧 E 𝑥 ↔ (𝐹𝑧) E (𝐹𝑥)))
7366, 70, 71, 72syl12anc 1321 . . . . . . . . . . . . . . . . . 18 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝑧 E 𝑥 ↔ (𝐹𝑧) E (𝐹𝑥)))
7465, 73mpbid 222 . . . . . . . . . . . . . . . . 17 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) E (𝐹𝑥))
7545epelc 4992 . . . . . . . . . . . . . . . . 17 ((𝐹𝑧) E (𝐹𝑥) ↔ (𝐹𝑧) ∈ (𝐹𝑥))
7674, 75sylib 208 . . . . . . . . . . . . . . . 16 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → (𝐹𝑧) ∈ (𝐹𝑥))
7762, 76eqeltrrd 2699 . . . . . . . . . . . . . . 15 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) ∧ 𝑧𝑥) → 𝑧 ∈ (𝐹𝑥))
7856, 77impbida 876 . . . . . . . . . . . . . 14 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → (𝑧 ∈ (𝐹𝑥) ↔ 𝑧𝑥))
7978eqrdv 2619 . . . . . . . . . . . . 13 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 (𝐹𝑦) = 𝑦)) → (𝐹𝑥) = 𝑥)
8079expr 642 . . . . . . . . . . . 12 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝐹𝑦) = 𝑦 → (𝐹𝑥) = 𝑥))
8116, 80sylbid 230 . . . . . . . . . . 11 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥𝐴) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝐹𝑥) = 𝑥))
8281ex 450 . . . . . . . . . 10 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝐹𝑥) = 𝑥)))
8382com23 86 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
8483a2i 14 . . . . . . . 8 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
8584a1i 11 . . . . . . 7 (𝑥 ∈ On → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦𝑥 (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))))
8610, 85syl5bi 232 . . . . . 6 (𝑥 ∈ On → (∀𝑦𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦𝐴 → (𝐹𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))))
879, 86tfis2 7010 . . . . 5 (𝑥 ∈ On → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥)))
8887com3l 89 . . . 4 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝑥 ∈ On → (𝐹𝑥) = 𝑥)))
893, 88mpdd 43 . . 3 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥𝐴 → (𝐹𝑥) = 𝑥))
9089ralrimiv 2960 . 2 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑥𝐴 (𝐹𝑥) = 𝑥)
91 fveq2 6153 . . . . . . . . 9 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
92 id 22 . . . . . . . . 9 (𝑥 = 𝑧𝑥 = 𝑧)
9391, 92eqeq12d 2636 . . . . . . . 8 (𝑥 = 𝑧 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑧) = 𝑧))
9493rspccva 3297 . . . . . . 7 ((∀𝑥𝐴 (𝐹𝑥) = 𝑥𝑧𝐴) → (𝐹𝑧) = 𝑧)
9594adantll 749 . . . . . 6 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → (𝐹𝑧) = 𝑧)
96 ffvelrn 6318 . . . . . . . . 9 ((𝐹:𝐴𝐵𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
9723, 96sylan 488 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
98973ad2antl1 1221 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
9998adantlr 750 . . . . . 6 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
10095, 99eqeltrrd 2699 . . . . 5 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) ∧ 𝑧𝐴) → 𝑧𝐵)
101100ex 450 . . . 4 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐴𝑧𝐵))
102 simpl1 1062 . . . . . . . 8 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
103 f1ofo 6106 . . . . . . . . 9 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
104 forn 6080 . . . . . . . . 9 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
10517, 103, 1043syl 18 . . . . . . . 8 (𝐹 Isom E , E (𝐴, 𝐵) → ran 𝐹 = 𝐵)
106102, 105syl 17 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → ran 𝐹 = 𝐵)
107106eleq2d 2684 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹𝑧𝐵))
108 f1ofn 6100 . . . . . . . . . 10 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
10917, 108syl 17 . . . . . . . . 9 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
1101093ad2ant1 1080 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹 Fn 𝐴)
111110adantr 481 . . . . . . 7 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐹 Fn 𝐴)
112 fvelrnb 6205 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
113111, 112syl 17 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
114107, 113bitr3d 270 . . . . 5 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐵 ↔ ∃𝑤𝐴 (𝐹𝑤) = 𝑧))
115 fveq2 6153 . . . . . . . . . . . 12 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
116 id 22 . . . . . . . . . . . 12 (𝑥 = 𝑤𝑥 = 𝑤)
117115, 116eqeq12d 2636 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐹𝑥) = 𝑥 ↔ (𝐹𝑤) = 𝑤))
118117rspcv 3294 . . . . . . . . . 10 (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝐹𝑤) = 𝑤))
119118a1i 11 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝐹𝑤) = 𝑤)))
120 simpr 477 . . . . . . . . . . . . 13 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑧)
121 simpl 473 . . . . . . . . . . . . 13 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → (𝐹𝑤) = 𝑤)
122120, 121eqtr3d 2657 . . . . . . . . . . . 12 (((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧) → 𝑧 = 𝑤)
123122adantl 482 . . . . . . . . . . 11 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑧 = 𝑤)
124 simplr 791 . . . . . . . . . . 11 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑤𝐴)
125123, 124eqeltrd 2698 . . . . . . . . . 10 ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤𝐴) ∧ ((𝐹𝑤) = 𝑤 ∧ (𝐹𝑤) = 𝑧)) → 𝑧𝐴)
126125exp43 639 . . . . . . . . 9 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → ((𝐹𝑤) = 𝑤 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
127119, 126syldd 72 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤𝐴 → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
128127com23 86 . . . . . . 7 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑥𝐴 (𝐹𝑥) = 𝑥 → (𝑤𝐴 → ((𝐹𝑤) = 𝑧𝑧𝐴))))
129128imp 445 . . . . . 6 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑤𝐴 → ((𝐹𝑤) = 𝑧𝑧𝐴)))
130129rexlimdv 3024 . . . . 5 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (∃𝑤𝐴 (𝐹𝑤) = 𝑧𝑧𝐴))
131114, 130sylbid 230 . . . 4 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐵𝑧𝐴))
132101, 131impbid 202 . . 3 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → (𝑧𝐴𝑧𝐵))
133132eqrdv 2619 . 2 (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥𝐴 (𝐹𝑥) = 𝑥) → 𝐴 = 𝐵)
13490, 133mpdan 701 1 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  wss 3559   class class class wbr 4618   E cep 4988  ccnv 5078  ran crn 5080  Ord word 5686  Oncon0 5687   Fn wfn 5847  wf 5848  ontowfo 5850  1-1-ontowf1o 5851  cfv 5852   Isom wiso 5853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-ord 5690  df-on 5691  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861
This theorem is referenced by:  ordiso  8372  oieu  8395  oiid  8397
  Copyright terms: Public domain W3C validator