ordiso2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ordiso2		GIF version

Theorem ordiso2 7110

Description: Generalize ordiso 7111 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 4529	. . . . . 6 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
2	1	3ad2ant2 1021	. . . . 5 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 ⊆ On)
3	2	sseld 3183	. . . 4 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → 𝑥 ∈ On))
4		eleq1 2259	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
5		fveq2 5561	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
6		id 19	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦)
7	5, 6	eqeq12d 2211	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑦) = 𝑦))
8	4, 7	imbi12d 234	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥) ↔ (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)))
9	8	imbi2d 230	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦))))
10		r19.21v 2574	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) ↔ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)))
11		ordelss 4415	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴)
12	11	3ad2antl2 1162	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐴)
13	12	sselda 3184	. . . . . . . . . . . . . 14 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝐴)
14		pm5.5 242	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐴 → ((𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ (𝐹‘𝑦) = 𝑦))
15	13, 14	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝑥) → ((𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ (𝐹‘𝑦) = 𝑦))
16	15	ralbidva 2493	. . . . . . . . . . . 12 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦))
17		isof1o 5857	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
18	17	3ad2ant1 1020	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴–1-1-onto→𝐵)
19	18	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹:𝐴–1-1-onto→𝐵)
20		simpll3 1040	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → Ord 𝐵)
21		simpr 110	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ (𝐹‘𝑥))
22		f1of 5507	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
23	17, 22	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴⟶𝐵)
24	23	3ad2ant1 1020	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹:𝐴⟶𝐵)
25	24	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹:𝐴⟶𝐵)
26		simplrl 535	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑥 ∈ 𝐴)
27	25, 26	ffvelcdmd 5701	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ 𝐵)
28	21, 27	jca 306	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝑧 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝐵))
29		ordtr1 4424	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝐵 → ((𝑧 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝐵) → 𝑧 ∈ 𝐵))
30	20, 28, 29	sylc 62	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ 𝐵)
31		f1ocnvfv2 5828	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
32	19, 30, 31	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(^◡𝐹‘𝑧)) = 𝑧)
33	32, 21	eqeltrd 2273	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹‘𝑥))
34		simpll1 1038	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝐹 Isom E , E (𝐴, 𝐵))
35		f1ocnv 5520	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ^◡𝐹:𝐵–1-1-onto→𝐴)
36		f1of 5507	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (^◡𝐹:𝐵–1-1-onto→𝐴 → ^◡𝐹:𝐵⟶𝐴)
37	19, 35, 36	3syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ^◡𝐹:𝐵⟶𝐴)
38	37, 30	ffvelcdmd 5701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (^◡𝐹‘𝑧) ∈ 𝐴)
39		isorel 5858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ ((^◡𝐹‘𝑧) ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → ((^◡𝐹‘𝑧) E 𝑥 ↔ (𝐹‘(^◡𝐹‘𝑧)) E (𝐹‘𝑥)))
40	34, 38, 26, 39	syl12anc 1247	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((^◡𝐹‘𝑧) E 𝑥 ↔ (𝐹‘(^◡𝐹‘𝑧)) E (𝐹‘𝑥)))
41		vex 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑥 ∈ V
42	41	epelc 4327	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((^◡𝐹‘𝑧) E 𝑥 ↔ (^◡𝐹‘𝑧) ∈ 𝑥)
43	42	a1i 9	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((^◡𝐹‘𝑧) E 𝑥 ↔ (^◡𝐹‘𝑧) ∈ 𝑥))
44		f1ofn 5508	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
45	17, 44	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹 Fn 𝐴)
46		funfvex 5578	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ V)
47	46	funfni 5361	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ V)
48	45, 47	sylan 283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ V)
49	34, 26, 48	syl2anc 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ V)
50		epelg 4326	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑥) ∈ V → ((𝐹‘(^◡𝐹‘𝑧)) E (𝐹‘𝑥) ↔ (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹‘𝑥)))
51	49, 50	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((𝐹‘(^◡𝐹‘𝑧)) E (𝐹‘𝑥) ↔ (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹‘𝑥)))
52	40, 43, 51	3bitr3d 218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ((^◡𝐹‘𝑧) ∈ 𝑥 ↔ (𝐹‘(^◡𝐹‘𝑧)) ∈ (𝐹‘𝑥)))
53	33, 52	mpbird 167	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (^◡𝐹‘𝑧) ∈ 𝑥)
54		simplrr 536	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)
55		fveq2 5561	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (^◡𝐹‘𝑧) → (𝐹‘𝑦) = (𝐹‘(^◡𝐹‘𝑧)))
56		id 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (^◡𝐹‘𝑧) → 𝑦 = (^◡𝐹‘𝑧))
57	55, 56	eqeq12d 2211	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (^◡𝐹‘𝑧) → ((𝐹‘𝑦) = 𝑦 ↔ (𝐹‘(^◡𝐹‘𝑧)) = (^◡𝐹‘𝑧)))
58	57	rspcv 2864	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝐹‘𝑧) ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 → (𝐹‘(^◡𝐹‘𝑧)) = (^◡𝐹‘𝑧)))
59	53, 54, 58	sylc 62	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → (𝐹‘(^◡𝐹‘𝑧)) = (^◡𝐹‘𝑧))
60	32, 59	eqtr3d 2231	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 = (^◡𝐹‘𝑧))
61	60, 53	eqeltrd 2273	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ (𝐹‘𝑥)) → 𝑧 ∈ 𝑥)
62		simprr 531	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)
63		fveq2 5561	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧))
64		id 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
65	63, 64	eqeq12d 2211	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) = 𝑦 ↔ (𝐹‘𝑧) = 𝑧))
66	65	rspccva 2867	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) = 𝑧)
67	62, 66	sylan 283	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) = 𝑧)
68		epel 4328	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 E 𝑥 ↔ 𝑧 ∈ 𝑥)
69	68	biimpri 133	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑥 → 𝑧 E 𝑥)
70	69	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 E 𝑥)
71		simpll1 1038	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
72		simpl2 1003	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → Ord 𝐴)
73		simprl 529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → 𝑥 ∈ 𝐴)
74	72, 73, 11	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → 𝑥 ⊆ 𝐴)
75	74	sselda 3184	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝐴)
76		simplrl 535	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝐴)
77		isorel 5858	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑧 E 𝑥 ↔ (𝐹‘𝑧) E (𝐹‘𝑥)))
78	71, 75, 76, 77	syl12anc 1247	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝑧 E 𝑥 ↔ (𝐹‘𝑧) E (𝐹‘𝑥)))
79	70, 78	mpbid 147	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) E (𝐹‘𝑥))
80	71, 76, 48	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑥) ∈ V)
81		epelg 4326	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑥) ∈ V → ((𝐹‘𝑧) E (𝐹‘𝑥) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑥)))
82	80, 81	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → ((𝐹‘𝑧) E (𝐹‘𝑥) ↔ (𝐹‘𝑧) ∈ (𝐹‘𝑥)))
83	79, 82	mpbid 147	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → (𝐹‘𝑧) ∈ (𝐹‘𝑥))
84	67, 83	eqeltrrd 2274	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝐹‘𝑥))
85	61, 84	impbida 596	. . . . . . . . . . . . . 14 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → (𝑧 ∈ (𝐹‘𝑥) ↔ 𝑧 ∈ 𝑥))
86	85	eqrdv 2194	. . . . . . . . . . . . 13 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦)) → (𝐹‘𝑥) = 𝑥)
87	86	expr 375	. . . . . . . . . . . 12 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝐹‘𝑦) = 𝑦 → (𝐹‘𝑥) = 𝑥))
88	16, 87	sylbid 150	. . . . . . . . . . 11 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝐹‘𝑥) = 𝑥))
89	88	ex 115	. . . . . . . . . 10 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝐹‘𝑥) = 𝑥)))
90	89	com23 78	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
91	90	a2i 11	. . . . . . . 8 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
92	91	a1i 9	. . . . . . 7 ⊢ (𝑥 ∈ On → (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))))
93	10, 92	biimtrid 152	. . . . . 6 ⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = 𝑦)) → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))))
94	9, 93	tfis2 4622	. . . . 5 ⊢ (𝑥 ∈ On → ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥)))
95	94	com3l 81	. . . 4 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝑥 ∈ On → (𝐹‘𝑥) = 𝑥)))
96	3, 95	mpdd 41	. . 3 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) = 𝑥))
97	96	ralrimiv 2569	. 2 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥)
98		fveq2 5561	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
99		id 19	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧)
100	98, 99	eqeq12d 2211	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑧) = 𝑧))
101	100	rspccva 2867	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝑧)
102	101	adantll 476	. . . . . 6 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = 𝑧)
103	23	ffvelcdmda 5700	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
104	103	3ad2antl1 1161	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
105	104	adantlr 477	. . . . . 6 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
106	102, 105	eqeltrrd 2274	. . . . 5 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵)
107	106	ex 115	. . . 4 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))
108		simpl1 1002	. . . . . . . 8 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐹 Isom E , E (𝐴, 𝐵))
109		f1ofo 5514	. . . . . . . . 9 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵)
110		forn 5486	. . . . . . . . 9 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
111	17, 109, 110	3syl 17	. . . . . . . 8 ⊢ (𝐹 Isom E , E (𝐴, 𝐵) → ran 𝐹 = 𝐵)
112	108, 111	syl 14	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → ran 𝐹 = 𝐵)
113	112	eleq2d 2266	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐵))
114	45	3ad2ant1 1020	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐹 Fn 𝐴)
115	114	adantr 276	. . . . . . 7 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐹 Fn 𝐴)
116		fvelrnb 5611	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
117	115, 116	syl 14	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
118	113, 117	bitr3d 190	. . . . 5 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐵 ↔ ∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧))
119		fveq2 5561	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤))
120		id 19	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤)
121	119, 120	eqeq12d 2211	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) = 𝑥 ↔ (𝐹‘𝑤) = 𝑤))
122	121	rspcv 2864	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝐹‘𝑤) = 𝑤))
123	122	a1i 9	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝐹‘𝑤) = 𝑤)))
124		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑧)
125		simpl 109	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → (𝐹‘𝑤) = 𝑤)
126	124, 125	eqtr3d 2231	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧) → 𝑧 = 𝑤)
127	126	adantl 277	. . . . . . . . . . 11 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑧 = 𝑤)
128		simplr 528	. . . . . . . . . . 11 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑤 ∈ 𝐴)
129	127, 128	eqeltrd 2273	. . . . . . . . . 10 ⊢ ((((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ 𝑤 ∈ 𝐴) ∧ ((𝐹‘𝑤) = 𝑤 ∧ (𝐹‘𝑤) = 𝑧)) → 𝑧 ∈ 𝐴)
130	129	exp43 372	. . . . . . . . 9 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑤 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
131	123, 130	syldd 67	. . . . . . . 8 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
132	131	com23 78	. . . . . . 7 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥 → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))))
133	132	imp 124	. . . . . 6 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑤 ∈ 𝐴 → ((𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴)))
134	133	rexlimdv 2613	. . . . 5 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (∃𝑤 ∈ 𝐴 (𝐹‘𝑤) = 𝑧 → 𝑧 ∈ 𝐴))
135	118, 134	sylbid 150	. . . 4 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐴))
136	107, 135	impbid 129	. . 3 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵))
137	136	eqrdv 2194	. 2 ⊢ (((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑥) → 𝐴 = 𝐵)
138	97, 137	mpdan 421	1 ⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ Ord 𝐵) → 𝐴 = 𝐵)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 980 = wceq 1364 ∈ wcel 2167 ∀wral 2475 ∃wrex 2476 Vcvv 2763 ⊆ wss 3157 class class class wbr 4034 E cep 4323 Ord word 4398 Oncon0 4399 ^◡ccnv 4663 ran crn 4665 Fn wfn 5254 ⟶wf 5255 –onto→wfo 5257 –1-1-onto→wf1o 5258 ‘cfv 5259 Isom wiso 5260

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-pow 4208 ax-pr 4243 ax-setind 4574

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ral 2480 df-rex 2481 df-rab 2484 df-v 2765 df-sbc 2990 df-un 3161 df-in 3163 df-ss 3170 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-eprel 4325 df-id 4329 df-iord 4402 df-on 4404 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268

This theorem is referenced by: ordiso 7111

W3C validator