Theorem ordiso2 9473

Description: Generalize ordiso 9474 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 7778	. . . . . 6 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
2	1	3ad2ant2 1150	. . . . 5 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 ⊆ On)
3	2	sseld 3944	. . . 4 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
4		eleq1w 2852	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
5		fveq2 6879	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
6		id 23	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
7	5, 6	eqeq12d 2785	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑦) = 𝑦))
8	4, 7	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥) ↔ (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)))
9	8	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦))))
10		r19.21v 3196	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)))
11		ordelss 6373	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴)
12	11	3ad2antl2 1203	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴)
13	12	sselda 3945	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)
14		pm5.5 364	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐴 → ((𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ (𝐹‘𝑦) = 𝑦))
15	13, 14	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ (𝐹‘𝑦) = 𝑦))
16	15	ralbidva 3192	. . . . . . . . . . . 12 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦))
17		isof1o 7319	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
18	17	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
19	18	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹:𝐴–1-1-onto→𝐵)
20		simpll3 1231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → Ord 𝐵)
21		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ (𝐹‘𝑥))
22		f1of 6818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
23	17, 22	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴⟶𝐵)
24	23	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴⟶𝐵)
25	24	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹:𝐴⟶𝐵)
26		simplrl 788	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑥 ∈ 𝐴)
27	25, 26	ffvelcdmd 7078	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ 𝐵)
28	21, 27	jca 520	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝑧 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝐵))
29		ordtr1 6402	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝐵 → ((𝑧 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝐵) → 𝑧 ∈ 𝐵))
30	20, 28, 29	sylc 66	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ 𝐵)
31		f1ocnvfv2 7273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧)
32	19, 30, 31	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧)
33	32, 21	eqeltrd 2869	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥))
34		simpll1 1229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹 Isom E , E (𝐴, 𝐵))
35		f1ocnv 6831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
36		f1of 6818	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
37	19, 35, 36	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ◡𝐹:𝐵⟶𝐴)
38	37, 30	ffvelcdmd 7078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (◡𝐹‘𝑧) ∈ 𝐴)
39		isorel 7322	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ ((◡𝐹‘𝑧) ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((◡𝐹‘𝑧) E 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥)))
40	34, 38, 26, 39	syl12anc 849	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((◡𝐹‘𝑧) E 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥)))
41		epel 5562	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐹‘𝑧) E 𝑥 ↔ (◡𝐹‘𝑧) ∈ 𝑥)
42		fvex 6892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑥) ∈ V
43	42	epeli 5561	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥) ↔ (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥))
44	40, 41, 43	3bitr3g 316	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((◡𝐹‘𝑧) ∈ 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥)))
45	33, 44	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (◡𝐹‘𝑧) ∈ 𝑥)
46		simplrr 789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)
47		fveq2 6879	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(◡𝐹‘𝑧)))
48		id 23	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (◡𝐹‘𝑧) → 𝑦 = (◡𝐹‘𝑧))
49	47, 48	eqeq12d 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (◡𝐹‘𝑧) → ((𝐹‘𝑦) = 𝑦 ↔ (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧)))
50	49	rspcv 3586	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝐹‘𝑧) ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 → (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧)))
51	45, 46, 50	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧))
52	32, 51	eqtr3d 2806	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 = (◡𝐹‘𝑧))
53	52, 45	eqeltrd 2869	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ 𝑥)
54		simprr 784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)
55		fveq2 6879	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
56		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
57	55, 56	eqeq12d 2785	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) = 𝑦 ↔ (𝐹‘𝑧) = 𝑧))
58	57	rspccva 3589	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) = 𝑧)
59	54, 58	sylan 591	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) = 𝑧)
60		epel 5562	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 E 𝑥 ↔ 𝑧 ∈ 𝑥)
61	60	bilanri 511	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 E 𝑥)
62		simpll1 1229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
63		simpl2 1209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → Ord 𝐴)
64		simprl 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → 𝑥 ∈ 𝐴)
65	63, 64, 11	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → 𝑥 ⊆ 𝐴)
66	65	sselda 3945	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝐴)
67		simplrl 788	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝐴)
68		isorel 7322	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑧 E 𝑥 ↔ (𝐹‘𝑧) E (𝐹‘𝑥)))
69	62, 66, 67, 68	syl12anc 849	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝑧 E 𝑥 ↔ (𝐹‘𝑧) E (𝐹‘𝑥)))
70	61, 69	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) E (𝐹‘𝑥))
71	42	epeli 5561	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑧) E (𝐹‘𝑥) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑥))
72	70, 71	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) ∈ (𝐹‘𝑥))
73	59, 72	eqeltrrd 2870	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝐹‘𝑥))
74	53, 73	impbida 812	. . . . . . . . . . . . . 14 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → (𝑧 ∈ (𝐹‘𝑥) ↔ 𝑧 ∈ 𝑥))
75	74	eqrdv 2767	. . . . . . . . . . . . 13 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → (𝐹‘𝑥) = 𝑥)
76	75	expr 461	. . . . . . . . . . . 12 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 → (𝐹‘𝑥) = 𝑥))
77	16, 76	sylbid 243	. . . . . . . . . . 11 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝐹‘𝑥) = 𝑥))
78	77	ex 417	. . . . . . . . . 10 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝐹‘𝑥) = 𝑥)))
79	78	com23 87	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
80	79	a2i 15	. . . . . . . 8 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
81	80	a1i 11	. . . . . . 7 ⊢ (𝑥 ∈ On → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))))
82	10, 81	biimtrid 245	. . . . . 6 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))))
83	9, 82	tfis2 7849	. . . . 5 ⊢ (𝑥 ∈ On → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
84	83	com3l 90	. . . 4 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ On → (𝐹‘𝑥) = 𝑥)))
85	3, 84	mpdd 44	. . 3 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))
86	85	ralrimiv 3162	. 2 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥)
87		fveq2 6879	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
88		id 23	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
89	87, 88	eqeq12d 2785	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑧) = 𝑧))
90	89	rspccva 3589	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝑧)
91	90	adantll 726	. . . . . 6 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝑧)
92	23	ffvelcdmda 7077	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
93	92	3ad2antl1 1202	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
94	93	adantlr 727	. . . . . 6 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
95	91, 94	eqeltrrd 2870	. . . . 5 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵)
96	95	ex 417	. . . 4 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))
97		simpl1 1208	. . . . . . . 8 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
98		f1ofo 6826	. . . . . . . . 9 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)
99		forn 6793	. . . . . . . . 9 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
100	17, 98, 99	3syl 19	. . . . . . . 8 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ran 𝐹 = 𝐵)
101	97, 100	syl 18	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → ran 𝐹 = 𝐵)
102	101	eleq2d 2855	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐵))
103		f1ofn 6819	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
104	17, 103	syl 18	. . . . . . . . 9 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
105	104	3ad2ant1 1149	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹 Fn 𝐴)
106	105	adantr 485	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐹 Fn 𝐴)
107		fvelrnb 6939	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
108	106, 107	syl 18	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
109	102, 108	bitr3d 284	. . . . 5 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐵 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
110		fveq2 6879	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
111		id 23	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤)
112	110, 111	eqeq12d 2785	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑤) = 𝑤))
113	112	rspcv 3586	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝐹‘𝑤) = 𝑤))
114	113	a1i 11	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝐹‘𝑤) = 𝑤)))
115		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑧)
116		simpl 487	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑤)
117	115, 116	eqtr3d 2806	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → 𝑧 = 𝑤)
118	117	adantl 486	. . . . . . . . . . 11 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑧 = 𝑤)
119		simplr 780	. . . . . . . . . . 11 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑤 ∈ 𝐴)
120	118, 119	eqeltrd 2869	. . . . . . . . . 10 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑧 ∈ 𝐴)
121	120	exp43 441	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑤 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
122	114, 121	syldd 73	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
123	122	com23 87	. . . . . . 7 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
124	123	imp 411	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴)))
125	124	rexlimdv 3170	. . . . 5 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))
126	109, 125	sylbid 243	. . . 4 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐴))
127	96, 126	impbid 215	. . 3 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵))
128	127	eqrdv 2767	. 2 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐴 = 𝐵)
129	86, 128	mpdan 699	1 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095   ⊆ wss 3913   class class class wbr 5110   E cep 5558  ^◡ccnv 5658  ran crn 5660  Ord word 6356  Oncon0 6357   Fn wfn 6528  ⟶wf 6529  –onto→wfo 6531  –1-1-onto→wf1o 6532  ‘cfv 6533   Isom wiso 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6360  df-on 6361  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542

This theorem is referenced by:  ordiso  9474  oieu  9497  oiid  9499