This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordiso2

Description: Generalize ordiso to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion ordiso2 ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 ordsson ⊢ ( Ord 𝐴 → 𝐴 ⊆ On )
2 1 3ad2ant2 ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → 𝐴 ⊆ On )
3 2 sseld ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ On ) )
4 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
5 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
6 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
7 5 6 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ↔ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) )
8 4 7 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) )
9 8 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) ↔ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ) )
10 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ↔ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) )
11 ordelss ⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ 𝐴 )
12 11 3ad2antl2 ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ 𝐴 )
13 12 sselda ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐴 )
14 pm5.5 ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) )
15 13 14 syl ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) )
16 15 ralbidva ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) )
17 isof1o ⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
18 17 3ad2ant1 ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
19 18 ad2antrr ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
20 simpll3 ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → Ord 𝐵 )
21 simpr ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) )
22 f1of ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
23 17 22 syl ⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
24 23 3ad2ant1 ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
25 24 ad2antrr ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
26 simplrl ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑥 ∈ 𝐴 )
27 25 26 ffvelcdmd ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
28 21 27 jca ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
29 ordtr1 ⊢ ( Ord 𝐵 → ( ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → 𝑧 ∈ 𝐵 ) )
30 20 28 29 sylc ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑧 ∈ 𝐵 )
31 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
32 19 30 31 syl2anc ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
33 32 21 eqeltrd ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 ‘ 𝑥 ) )
34 simpll1 ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝐹 Isom E , E ( 𝐴 , 𝐵 ) )
35 f1ocnv ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
36 f1of ⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐵 ⟶ 𝐴 )
37 19 35 36 3syl ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ◡ 𝐹 : 𝐵 ⟶ 𝐴 )
38 37 30 ffvelcdmd ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝐴 )
39 isorel ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) E 𝑥 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) E ( 𝐹 ‘ 𝑥 ) ) )
40 34 38 26 39 syl12anc ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) E 𝑥 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) E ( 𝐹 ‘ 𝑥 ) ) )
41 epel ⊢ ( ( ◡ 𝐹 ‘ 𝑧 ) E 𝑥 ↔ ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑥 )
42 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
43 42 epeli ⊢ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) E ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 ‘ 𝑥 ) )
44 40 41 43 3bitr3g ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑥 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ ( 𝐹 ‘ 𝑥 ) ) )
45 33 44 mpbird ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑥 )
46 simplrr ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 )
47 fveq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑧 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) )
48 id ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑧 ) → 𝑦 = ( ◡ 𝐹 ‘ 𝑧 ) )
49 47 48 eqeq12d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑧 ) → ( ( 𝐹 ‘ 𝑦 ) = 𝑦 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = ( ◡ 𝐹 ‘ 𝑧 ) ) )
50 49 rspcv ⊢ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = ( ◡ 𝐹 ‘ 𝑧 ) ) )
51 45 46 50 sylc ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = ( ◡ 𝐹 ‘ 𝑧 ) )
52 32 51 eqtr3d ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑧 = ( ◡ 𝐹 ‘ 𝑧 ) )
53 52 45 eqeltrd ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑧 ∈ 𝑥 )
54 simprr ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 )
55 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
56 id ⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 )
57 55 56 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) = 𝑧 ) )
58 57 rspccva ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ∧ 𝑧 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑧 ) = 𝑧 )
59 54 58 sylan ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑧 ) = 𝑧 )
60 epel ⊢ ( 𝑧 E 𝑥 ↔ 𝑧 ∈ 𝑥 )
61 60 biimpri ⊢ ( 𝑧 ∈ 𝑥 → 𝑧 E 𝑥 )
62 61 adantl ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ 𝑥 ) → 𝑧 E 𝑥 )
63 simpll1 ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ 𝑥 ) → 𝐹 Isom E , E ( 𝐴 , 𝐵 ) )
64 simpl2 ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → Ord 𝐴 )
65 simprl ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 ∈ 𝐴 )
66 64 65 11 syl2anc ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 ⊆ 𝐴 )
67 66 sselda ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝐴 )
68 simplrl ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ 𝑥 ) → 𝑥 ∈ 𝐴 )
69 isorel ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑧 E 𝑥 ↔ ( 𝐹 ‘ 𝑧 ) E ( 𝐹 ‘ 𝑥 ) ) )
70 63 67 68 69 syl12anc ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝑧 E 𝑥 ↔ ( 𝐹 ‘ 𝑧 ) E ( 𝐹 ‘ 𝑥 ) ) )
71 62 70 mpbid ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑧 ) E ( 𝐹 ‘ 𝑥 ) )
72 42 epeli ⊢ ( ( 𝐹 ‘ 𝑧 ) E ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑥 ) )
73 71 72 sylib ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑥 ) )
74 59 73 eqeltrrd ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) ∧ 𝑧 ∈ 𝑥 ) → 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) )
75 53 74 impbida ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝑧 ∈ 𝑥 ) )
76 75 eqrdv ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 )
77 76 expr ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝑦 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
78 16 77 sylbid ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
79 78 ex ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) )
80 79 com23 ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) )
81 80 a2i ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) )
82 81 a1i ⊢ ( 𝑥 ∈ On → ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) ) )
83 10 82 biimtrid ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) ) )
84 9 83 tfis2 ⊢ ( 𝑥 ∈ On → ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) )
85 84 com3l ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ On → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) )
86 3 85 mpdd ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
87 86 ralrimiv ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 )
88 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
89 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
90 88 89 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ↔ ( 𝐹 ‘ 𝑧 ) = 𝑧 ) )
91 90 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = 𝑧 )
92 91 adantll ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = 𝑧 )
93 23 ffvelcdmda ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
94 93 3ad2antl1 ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
95 94 adantlr ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
96 92 95 eqeltrrd ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐵 )
97 96 ex ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) )
98 simpl1 ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → 𝐹 Isom E , E ( 𝐴 , 𝐵 ) )
99 f1ofo ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –onto→ 𝐵 )
100 forn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
101 17 99 100 3syl ⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → ran 𝐹 = 𝐵 )
102 98 101 syl ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ran 𝐹 = 𝐵 )
103 102 eleq2d ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ( 𝑧 ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐵 ) )
104 f1ofn ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 Fn 𝐴 )
105 17 104 syl ⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → 𝐹 Fn 𝐴 )
106 105 3ad2ant1 ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → 𝐹 Fn 𝐴 )
107 106 adantr ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → 𝐹 Fn 𝐴 )
108 fvelrnb ⊢ ( 𝐹 Fn 𝐴 → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
109 107 108 syl ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
110 103 109 bitr3d ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ( 𝑧 ∈ 𝐵 ↔ ∃ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
111 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
112 id ⊢ ( 𝑥 = 𝑤 → 𝑥 = 𝑤 )
113 111 112 eqeq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ↔ ( 𝐹 ‘ 𝑤 ) = 𝑤 ) )
114 113 rspcv ⊢ ( 𝑤 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 → ( 𝐹 ‘ 𝑤 ) = 𝑤 ) )
115 114 a1i ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑤 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 → ( 𝐹 ‘ 𝑤 ) = 𝑤 ) ) )
116 simpr ⊢ ( ( ( 𝐹 ‘ 𝑤 ) = 𝑤 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) → ( 𝐹 ‘ 𝑤 ) = 𝑧 )
117 simpl ⊢ ( ( ( 𝐹 ‘ 𝑤 ) = 𝑤 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) → ( 𝐹 ‘ 𝑤 ) = 𝑤 )
118 116 117 eqtr3d ⊢ ( ( ( 𝐹 ‘ 𝑤 ) = 𝑤 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑤 )
119 118 adantl ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑤 ) = 𝑤 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) → 𝑧 = 𝑤 )
120 simplr ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑤 ) = 𝑤 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) → 𝑤 ∈ 𝐴 )
121 119 120 eqeltrd ⊢ ( ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑤 ) = 𝑤 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) → 𝑧 ∈ 𝐴 )
122 121 exp43 ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑤 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑤 ) = 𝑤 → ( ( 𝐹 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ 𝐴 ) ) ) )
123 115 122 syldd ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑤 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 → ( ( 𝐹 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ 𝐴 ) ) ) )
124 123 com23 ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 → ( 𝑤 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ 𝐴 ) ) ) )
125 124 imp ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ( 𝑤 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ 𝐴 ) ) )
126 125 rexlimdv ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ( ∃ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) = 𝑧 → 𝑧 ∈ 𝐴 ) )
127 110 126 sylbid ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐴 ) )
128 97 127 impbid ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) )
129 128 eqrdv ⊢ ( ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → 𝐴 = 𝐵 )
130 87 129 mpdan ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ Ord 𝐵 ) → 𝐴 = 𝐵 )