Theorem ordiso2 8303

Description: Generalize ordiso 8304 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 6881	. . . . . 6 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
2	1	3ad2ant2 1076	. . . . 5 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 ⊆ On)
3	2	sseld 3567	. . . 4 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
4		eleq1 2676	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
5		fveq2 6103	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
6		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
7	5, 6	eqeq12d 2625	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑦) = 𝑦))
8	4, 7	imbi12d 333	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥) ↔ (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)))
9	8	imbi2d 329	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦))))
10		r19.21v 2943	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)))
11		ordelss 5656	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴)
12	11	3ad2antl2 1217	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴)
13	12	sselda 3568	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)
14		pm5.5 350	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐴 → ((𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ (𝐹‘𝑦) = 𝑦))
15	13, 14	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ (𝐹‘𝑦) = 𝑦))
16	15	ralbidva 2968	. . . . . . . . . . . 12 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦))
17		isof1o 6473	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
18	17	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
19	18	ad2antrr 758	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹:𝐴–1-1-onto→𝐵)
20		simpll3 1095	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → Ord 𝐵)
21		simpr 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ (𝐹‘𝑥))
22		f1of 6050	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
23	17, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴⟶𝐵)
24	23	3ad2ant1 1075	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴⟶𝐵)
25	24	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹:𝐴⟶𝐵)
26		simplrl 796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑥 ∈ 𝐴)
27		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
28	25, 26, 27	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ 𝐵)
29	21, 28	jca 553	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝑧 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝐵))
30		ordtr1 5684	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝐵 → ((𝑧 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝐵) → 𝑧 ∈ 𝐵))
31	20, 29, 30	sylc 63	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ 𝐵)
32		f1ocnvfv2 6433	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧)
33	19, 31, 32	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) = 𝑧)
34	33, 21	eqeltrd 2688	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥))
35		simpll1 1093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹 Isom E , E (𝐴, 𝐵))
36		f1ocnv 6062	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
37		f1of 6050	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
38	19, 36, 37	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ◡𝐹:𝐵⟶𝐴)
39		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → (◡𝐹‘𝑧) ∈ 𝐴)
40	38, 31, 39	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (◡𝐹‘𝑧) ∈ 𝐴)
41		isorel 6476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ ((◡𝐹‘𝑧) ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((◡𝐹‘𝑧) E 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥)))
42	35, 40, 26, 41	syl12anc 1316	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((◡𝐹‘𝑧) E 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥)))
43		vex 3176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑥 ∈ V
44	43	epelc 4951	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((◡𝐹‘𝑧) E 𝑥 ↔ (◡𝐹‘𝑧) ∈ 𝑥)
45		fvex 6113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹‘𝑥) ∈ V
46	45	epelc 4951	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘(◡𝐹‘𝑧)) E (𝐹‘𝑥) ↔ (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥))
47	42, 44, 46	3bitr3g 301	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((◡𝐹‘𝑧) ∈ 𝑥 ↔ (𝐹‘(◡𝐹‘𝑧)) ∈ (𝐹‘𝑥)))
48	34, 47	mpbird 246	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (◡𝐹‘𝑧) ∈ 𝑥)
49		simplrr 797	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)
50		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(◡𝐹‘𝑧)))
51		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (◡𝐹‘𝑧) → 𝑦 = (◡𝐹‘𝑧))
52	50, 51	eqeq12d 2625	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (◡𝐹‘𝑧) → ((𝐹‘𝑦) = 𝑦 ↔ (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧)))
53	52	rspcv 3278	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝐹‘𝑧) ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 → (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧)))
54	48, 49, 53	sylc 63	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(◡𝐹‘𝑧)) = (◡𝐹‘𝑧))
55	33, 54	eqtr3d 2646	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 = (◡𝐹‘𝑧))
56	55, 48	eqeltrd 2688	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ 𝑥)
57		simprr 792	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)
58		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
59		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
60	58, 59	eqeq12d 2625	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) = 𝑦 ↔ (𝐹‘𝑧) = 𝑧))
61	60	rspccva 3281	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) = 𝑧)
62	57, 61	sylan 487	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) = 𝑧)
63		epel 4952	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 E 𝑥 ↔ 𝑧 ∈ 𝑥)
64	63	biimpri 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑥 → 𝑧 E 𝑥)
65	64	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 E 𝑥)
66		simpll1 1093	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
67		simpl2 1058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → Ord 𝐴)
68		simprl 790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → 𝑥 ∈ 𝐴)
69	67, 68, 11	syl2anc 691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → 𝑥 ⊆ 𝐴)
70	69	sselda 3568	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝐴)
71		simplrl 796	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝐴)
72		isorel 6476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑧 E 𝑥 ↔ (𝐹‘𝑧) E (𝐹‘𝑥)))
73	66, 70, 71, 72	syl12anc 1316	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝑧 E 𝑥 ↔ (𝐹‘𝑧) E (𝐹‘𝑥)))
74	65, 73	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) E (𝐹‘𝑥))
75	45	epelc 4951	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑧) E (𝐹‘𝑥) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑥))
76	74, 75	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) ∈ (𝐹‘𝑥))
77	62, 76	eqeltrrd 2689	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝐹‘𝑥))
78	56, 77	impbida 873	. . . . . . . . . . . . . 14 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → (𝑧 ∈ (𝐹‘𝑥) ↔ 𝑧 ∈ 𝑥))
79	78	eqrdv 2608	. . . . . . . . . . . . 13 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → (𝐹‘𝑥) = 𝑥)
80	79	expr 641	. . . . . . . . . . . 12 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 → (𝐹‘𝑥) = 𝑥))
81	16, 80	sylbid 229	. . . . . . . . . . 11 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝐹‘𝑥) = 𝑥))
82	81	ex 449	. . . . . . . . . 10 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝐹‘𝑥) = 𝑥)))
83	82	com23 84	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
84	83	a2i 14	. . . . . . . 8 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
85	84	a1i 11	. . . . . . 7 ⊢ (𝑥 ∈ On → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))))
86	10, 85	syl5bi 231	. . . . . 6 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))))
87	9, 86	tfis2 6948	. . . . 5 ⊢ (𝑥 ∈ On → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
88	87	com3l 87	. . . 4 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ On → (𝐹‘𝑥) = 𝑥)))
89	3, 88	mpdd 42	. . 3 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))
90	89	ralrimiv 2948	. 2 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥)
91		fveq2 6103	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
92		id 22	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
93	91, 92	eqeq12d 2625	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑧) = 𝑧))
94	93	rspccva 3281	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝑧)
95	94	adantll 746	. . . . . 6 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝑧)
96		ffvelrn 6265	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
97	23, 96	sylan 487	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
98	97	3ad2antl1 1216	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
99	98	adantlr 747	. . . . . 6 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
100	95, 99	eqeltrrd 2689	. . . . 5 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵)
101	100	ex 449	. . . 4 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))
102		simpl1 1057	. . . . . . . 8 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
103		f1ofo 6057	. . . . . . . . 9 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)
104		forn 6031	. . . . . . . . 9 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
105	17, 103, 104	3syl 18	. . . . . . . 8 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ran 𝐹 = 𝐵)
106	102, 105	syl 17	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → ran 𝐹 = 𝐵)
107	106	eleq2d 2673	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐵))
108		f1ofn 6051	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
109	17, 108	syl 17	. . . . . . . . 9 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
110	109	3ad2ant1 1075	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹 Fn 𝐴)
111	110	adantr 480	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐹 Fn 𝐴)
112		fvelrnb 6153	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
113	111, 112	syl 17	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
114	107, 113	bitr3d 269	. . . . 5 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐵 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
115		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
116		id 22	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤)
117	115, 116	eqeq12d 2625	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑤) = 𝑤))
118	117	rspcv 3278	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝐹‘𝑤) = 𝑤))
119	118	a1i 11	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝐹‘𝑤) = 𝑤)))
120		simpr 476	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑧)
121		simpl 472	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑤)
122	120, 121	eqtr3d 2646	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → 𝑧 = 𝑤)
123	122	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑧 = 𝑤)
124		simplr 788	. . . . . . . . . . 11 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑤 ∈ 𝐴)
125	123, 124	eqeltrd 2688	. . . . . . . . . 10 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑧 ∈ 𝐴)
126	125	exp43 638	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑤 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
127	119, 126	syldd 70	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
128	127	com23 84	. . . . . . 7 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
129	128	imp 444	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴)))
130	129	rexlimdv 3012	. . . . 5 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))
131	114, 130	sylbid 229	. . . 4 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐴))
132	101, 131	impbid 201	. . 3 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵))
133	132	eqrdv 2608	. 2 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐴 = 𝐵)
134	90, 133	mpdan 699	1 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540   class class class wbr 4583   E cep 4947  ^◡ccnv 5037  ran crn 5039  Ord word 5639  Oncon0 5640   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813

This theorem is referenced by:  ordiso  8304  oieu  8327  oiid  8329