Theorem ordiso2 9451

Description: Generalize ordiso 9452 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 7717	. . . . . 6 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
2	1	3ad2ant2 1134	. . . . 5 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 ⊆ On)
3	2	sseld 3943	. . . 4 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
4		eleq1w 2820	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
5		fveq2 6842	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
6		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
7	5, 6	eqeq12d 2752	. . . . . . . 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 3176	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)))
11		ordelss 6333	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴)
12	11	3ad2antl2 1186	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴)
13	12	sselda 3944	. . . . . . . . . . . . . 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 3172	. . . . . . . . . . . 12 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦))
17		isof1o 7268	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
18	17	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
19	18	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹:𝐴–1-1-onto→𝐵)
20		simpll3 1214	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → Ord 𝐵)
21		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ (𝐹‘𝑥))
22		f1of 6784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
23	17, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴⟶𝐵)
24	23	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴⟶𝐵)
25	24	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹:𝐴⟶𝐵)
26		simplrl 775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑥 ∈ 𝐴)
27	25, 26	ffvelcdmd 7036	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ 𝐵)
28	21, 27	jca 512	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝑧 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝐵))
29		ordtr1 6360	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝐵 → ((𝑧 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝐵) → 𝑧 ∈ 𝐵))
30	20, 28, 29	sylc 65	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ 𝐵)
31		f1ocnvfv2 7223	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧)
32	19, 30, 31	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧)
33	32, 21	eqeltrd 2838	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥))
34		simpll1 1212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹 Isom E , E (𝐴, 𝐵))
35		f1ocnv 6796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
36		f1of 6784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
37	19, 35, 36	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ◡𝐹:𝐵⟶𝐴)
38	37, 30	ffvelcdmd 7036	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (◡𝐹‘𝑧) ∈ 𝐴)
39		isorel 7271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ ((◡𝐹‘𝑧) ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((◡𝐹‘𝑧) E 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥)))
40	34, 38, 26, 39	syl12anc 835	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((◡𝐹‘𝑧) E 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥)))
41		epel 5540	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐹‘𝑧) E 𝑥 ↔ (◡𝐹‘𝑧) ∈ 𝑥)
42		fvex 6855	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑥) ∈ V
43	42	epeli 5539	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥) ↔ (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥))
44	40, 41, 43	3bitr3g 312	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((◡𝐹‘𝑧) ∈ 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥)))
45	33, 44	mpbird 256	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (◡𝐹‘𝑧) ∈ 𝑥)
46		simplrr 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)
47		fveq2 6842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(◡𝐹‘𝑧)))
48		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (◡𝐹‘𝑧) → 𝑦 = (◡𝐹‘𝑧))
49	47, 48	eqeq12d 2752	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (◡𝐹‘𝑧) → ((𝐹‘𝑦) = 𝑦 ↔ (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧)))
50	49	rspcv 3577	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝐹‘𝑧) ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 → (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧)))
51	45, 46, 50	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧))
52	32, 51	eqtr3d 2778	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 = (◡𝐹‘𝑧))
53	52, 45	eqeltrd 2838	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ 𝑥)
54		simprr 771	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)
55		fveq2 6842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
56		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
57	55, 56	eqeq12d 2752	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) = 𝑦 ↔ (𝐹‘𝑧) = 𝑧))
58	57	rspccva 3580	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) = 𝑧)
59	54, 58	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) = 𝑧)
60		epel 5540	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 E 𝑥 ↔ 𝑧 ∈ 𝑥)
61	60	biimpri 227	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑥 → 𝑧 E 𝑥)
62	61	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 E 𝑥)
63		simpll1 1212	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
64		simpl2 1192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → Ord 𝐴)
65		simprl 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → 𝑥 ∈ 𝐴)
66	64, 65, 11	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → 𝑥 ⊆ 𝐴)
67	66	sselda 3944	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝐴)
68		simplrl 775	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝐴)
69		isorel 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑧 E 𝑥 ↔ (𝐹‘𝑧) E (𝐹‘𝑥)))
70	63, 67, 68, 69	syl12anc 835	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝑧 E 𝑥 ↔ (𝐹‘𝑧) E (𝐹‘𝑥)))
71	62, 70	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) E (𝐹‘𝑥))
72	42	epeli 5539	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑧) E (𝐹‘𝑥) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑥))
73	71, 72	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) ∈ (𝐹‘𝑥))
74	59, 73	eqeltrrd 2839	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝐹‘𝑥))
75	53, 74	impbida 799	. . . . . . . . . . . . . 14 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → (𝑧 ∈ (𝐹‘𝑥) ↔ 𝑧 ∈ 𝑥))
76	75	eqrdv 2734	. . . . . . . . . . . . 13 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → (𝐹‘𝑥) = 𝑥)
77	76	expr 457	. . . . . . . . . . . 12 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 → (𝐹‘𝑥) = 𝑥))
78	16, 77	sylbid 239	. . . . . . . . . . 11 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝐹‘𝑥) = 𝑥))
79	78	ex 413	. . . . . . . . . 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 241	. . . . . 6 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))))
84	9, 83	tfis2 7793	. . . . 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 3142	. 2 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥)
88		fveq2 6842	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
89		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
90	88, 89	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑧) = 𝑧))
91	90	rspccva 3580	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝑧)
92	91	adantll 712	. . . . . 6 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝑧)
93	23	ffvelcdmda 7035	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
94	93	3ad2antl1 1185	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
95	94	adantlr 713	. . . . . 6 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
96	92, 95	eqeltrrd 2839	. . . . 5 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵)
97	96	ex 413	. . . 4 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))
98		simpl1 1191	. . . . . . . 8 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
99		f1ofo 6791	. . . . . . . . 9 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)
100		forn 6759	. . . . . . . . 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 2823	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐵))
104		f1ofn 6785	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
105	17, 104	syl 17	. . . . . . . . 9 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
106	105	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹 Fn 𝐴)
107	106	adantr 481	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐹 Fn 𝐴)
108		fvelrnb 6903	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
109	107, 108	syl 17	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
110	103, 109	bitr3d 280	. . . . 5 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐵 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
111		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
112		id 22	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤)
113	111, 112	eqeq12d 2752	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑤) = 𝑤))
114	113	rspcv 3577	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝐹‘𝑤) = 𝑤))
115	114	a1i 11	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝐹‘𝑤) = 𝑤)))
116		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑧)
117		simpl 483	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑤)
118	116, 117	eqtr3d 2778	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → 𝑧 = 𝑤)
119	118	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑧 = 𝑤)
120		simplr 767	. . . . . . . . . . 11 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑤 ∈ 𝐴)
121	119, 120	eqeltrd 2838	. . . . . . . . . 10 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑧 ∈ 𝐴)
122	121	exp43 437	. . . . . . . . 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 407	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴)))
126	125	rexlimdv 3150	. . . . 5 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))
127	110, 126	sylbid 239	. . . 4 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐴))
128	97, 127	impbid 211	. . 3 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵))
129	128	eqrdv 2734	. 2 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐴 = 𝐵)
130	87, 129	mpdan 685	1 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3064  ∃wrex 3073   ⊆ wss 3910   class class class wbr 5105   E cep 5536  ^◡ccnv 5632  ran crn 5634  Ord word 6316  Oncon0 6317   Fn wfn 6491  ⟶wf 6492  –onto→wfo 6494  –1-1-onto→wf1o 6495  ‘cfv 6496   Isom wiso 6497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505

This theorem is referenced by:  ordiso  9452  oieu  9475  oiid  9477