Theorem ordiso2 9555

Description: Generalize ordiso 9556 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.

Step	Hyp	Ref	Expression
1		ordsson 7803	. . . . . 6 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
2	1	3ad2ant2 1135	. . . . 5 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 ⊆ On)
3	2	sseld 3982	. . . 4 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
4		eleq1w 2824	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
5		fveq2 6906	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
6		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
7	5, 6	eqeq12d 2753	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑦) = 𝑦))
8	4, 7	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥) ↔ (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)))
9	8	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦))))
10		r19.21v 3180	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)))
11		ordelss 6400	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴)
12	11	3ad2antl2 1187	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴)
13	12	sselda 3983	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)
14		pm5.5 361	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐴 → ((𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ (𝐹‘𝑦) = 𝑦))
15	13, 14	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ (𝐹‘𝑦) = 𝑦))
16	15	ralbidva 3176	. . . . . . . . . . . 12 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦))
17		isof1o 7343	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
18	17	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
19	18	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹:𝐴–1-1-onto→𝐵)
20		simpll3 1215	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → Ord 𝐵)
21		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ (𝐹‘𝑥))
22		f1of 6848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
23	17, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴⟶𝐵)
24	23	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴⟶𝐵)
25	24	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹:𝐴⟶𝐵)
26		simplrl 777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑥 ∈ 𝐴)
27	25, 26	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ 𝐵)
28	21, 27	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝑧 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝐵))
29		ordtr1 6427	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝐵 → ((𝑧 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝐵) → 𝑧 ∈ 𝐵))
30	20, 28, 29	sylc 65	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ 𝐵)
31		f1ocnvfv2 7297	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧)
32	19, 30, 31	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧)
33	32, 21	eqeltrd 2841	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥))
34		simpll1 1213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹 Isom E , E (𝐴, 𝐵))
35		f1ocnv 6860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
36		f1of 6848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
37	19, 35, 36	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ◡𝐹:𝐵⟶𝐴)
38	37, 30	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (◡𝐹‘𝑧) ∈ 𝐴)
39		isorel 7346	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ ((◡𝐹‘𝑧) ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((◡𝐹‘𝑧) E 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥)))
40	34, 38, 26, 39	syl12anc 837	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((◡𝐹‘𝑧) E 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥)))
41		epel 5587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐹‘𝑧) E 𝑥 ↔ (◡𝐹‘𝑧) ∈ 𝑥)
42		fvex 6919	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑥) ∈ V
43	42	epeli 5586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥) ↔ (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥))
44	40, 41, 43	3bitr3g 313	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((◡𝐹‘𝑧) ∈ 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥)))
45	33, 44	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (◡𝐹‘𝑧) ∈ 𝑥)
46		simplrr 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)
47		fveq2 6906	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(◡𝐹‘𝑧)))
48		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (◡𝐹‘𝑧) → 𝑦 = (◡𝐹‘𝑧))
49	47, 48	eqeq12d 2753	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (◡𝐹‘𝑧) → ((𝐹‘𝑦) = 𝑦 ↔ (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧)))
50	49	rspcv 3618	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝐹‘𝑧) ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 → (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧)))
51	45, 46, 50	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧))
52	32, 51	eqtr3d 2779	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 = (◡𝐹‘𝑧))
53	52, 45	eqeltrd 2841	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ 𝑥)
54		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)
55		fveq2 6906	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
56		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
57	55, 56	eqeq12d 2753	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) = 𝑦 ↔ (𝐹‘𝑧) = 𝑧))
58	57	rspccva 3621	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) = 𝑧)
59	54, 58	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) = 𝑧)
60		epel 5587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 E 𝑥 ↔ 𝑧 ∈ 𝑥)
61	60	biimpri 228	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑥 → 𝑧 E 𝑥)
62	61	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 E 𝑥)
63		simpll1 1213	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
64		simpl2 1193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → Ord 𝐴)
65		simprl 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → 𝑥 ∈ 𝐴)
66	64, 65, 11	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → 𝑥 ⊆ 𝐴)
67	66	sselda 3983	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝐴)
68		simplrl 777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝐴)
69		isorel 7346	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑧 E 𝑥 ↔ (𝐹‘𝑧) E (𝐹‘𝑥)))
70	63, 67, 68, 69	syl12anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝑧 E 𝑥 ↔ (𝐹‘𝑧) E (𝐹‘𝑥)))
71	62, 70	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) E (𝐹‘𝑥))
72	42	epeli 5586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑧) E (𝐹‘𝑥) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑥))
73	71, 72	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) ∈ (𝐹‘𝑥))
74	59, 73	eqeltrrd 2842	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝐹‘𝑥))
75	53, 74	impbida 801	. . . . . . . . . . . . . 14 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → (𝑧 ∈ (𝐹‘𝑥) ↔ 𝑧 ∈ 𝑥))
76	75	eqrdv 2735	. . . . . . . . . . . . 13 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → (𝐹‘𝑥) = 𝑥)
77	76	expr 456	. . . . . . . . . . . 12 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 → (𝐹‘𝑥) = 𝑥))
78	16, 77	sylbid 240	. . . . . . . . . . 11 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝐹‘𝑥) = 𝑥))
79	78	ex 412	. . . . . . . . . 10 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝐹‘𝑥) = 𝑥)))
80	79	com23 86	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
81	80	a2i 14	. . . . . . . 8 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
82	81	a1i 11	. . . . . . 7 ⊢ (𝑥 ∈ On → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))))
83	10, 82	biimtrid 242	. . . . . 6 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))))
84	9, 83	tfis2 7878	. . . . 5 ⊢ (𝑥 ∈ On → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
85	84	com3l 89	. . . 4 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ On → (𝐹‘𝑥) = 𝑥)))
86	3, 85	mpdd 43	. . 3 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))
87	86	ralrimiv 3145	. 2 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥)
88		fveq2 6906	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
89		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
90	88, 89	eqeq12d 2753	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑧) = 𝑧))
91	90	rspccva 3621	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝑧)
92	91	adantll 714	. . . . . 6 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝑧)
93	23	ffvelcdmda 7104	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
94	93	3ad2antl1 1186	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
95	94	adantlr 715	. . . . . 6 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
96	92, 95	eqeltrrd 2842	. . . . 5 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵)
97	96	ex 412	. . . 4 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))
98		simpl1 1192	. . . . . . . 8 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
99		f1ofo 6855	. . . . . . . . 9 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)
100		forn 6823	. . . . . . . . 9 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
101	17, 99, 100	3syl 18	. . . . . . . 8 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ran 𝐹 = 𝐵)
102	98, 101	syl 17	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → ran 𝐹 = 𝐵)
103	102	eleq2d 2827	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐵))
104		f1ofn 6849	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
105	17, 104	syl 17	. . . . . . . . 9 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
106	105	3ad2ant1 1134	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹 Fn 𝐴)
107	106	adantr 480	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐹 Fn 𝐴)
108		fvelrnb 6969	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
109	107, 108	syl 17	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
110	103, 109	bitr3d 281	. . . . 5 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐵 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
111		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
112		id 22	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤)
113	111, 112	eqeq12d 2753	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑤) = 𝑤))
114	113	rspcv 3618	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝐹‘𝑤) = 𝑤))
115	114	a1i 11	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝐹‘𝑤) = 𝑤)))
116		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑧)
117		simpl 482	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑤)
118	116, 117	eqtr3d 2779	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → 𝑧 = 𝑤)
119	118	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑧 = 𝑤)
120		simplr 769	. . . . . . . . . . 11 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑤 ∈ 𝐴)
121	119, 120	eqeltrd 2841	. . . . . . . . . 10 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑧 ∈ 𝐴)
122	121	exp43 436	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑤 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
123	115, 122	syldd 72	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
124	123	com23 86	. . . . . . 7 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
125	124	imp 406	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴)))
126	125	rexlimdv 3153	. . . . 5 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))
127	110, 126	sylbid 240	. . . 4 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐴))
128	97, 127	impbid 212	. . 3 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵))
129	128	eqrdv 2735	. 2 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐴 = 𝐵)
130	87, 129	mpdan 687	1 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070   ⊆ wss 3951   class class class wbr 5143   E cep 5583  ^◡ccnv 5684  ran crn 5686  Ord word 6383  Oncon0 6384   Fn wfn 6556  ⟶wf 6557  –onto→wfo 6559  –1-1-onto→wf1o 6560  ‘cfv 6561   Isom wiso 6562

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570

This theorem is referenced by:  ordiso  9556  oieu  9579  oiid  9581