Theorem ordtype 5691

Description: For any well-ordered set, there is an isomorphic ordinal number called its order type. (Contributed by Jeff Hankins, 17-Oct-2009.)

Assertion

Ref	Expression
ordtype	|- ((A e. B /\ R We A) -> E!x e. On E.f f Isom _E , R (x, A))

Distinct variable groups:   x,f,A   B,f,x   R,f,x

Proof of Theorem ordtype

Step	Hyp	Ref	Expression
1		weeq2 3647	. . . . . 6 |- (a = A -> (R We a <-> R We A))
2		isoeq5 4867	. . . . . . . 8 |- (a = A -> (f Isom _E , R (x, a) <-> f Isom _E , R (x, A)))
3	2	exbidv 1657	. . . . . . 7 |- (a = A -> (E.f f Isom _E , R (x, a) <-> E.f f Isom _E , R (x, A)))
4	3	rexbidv 2124	. . . . . 6 |- (a = A -> (E.x e. On E.f f Isom _E , R (x, a) <-> E.x e. On E.f f Isom _E , R (x, A)))
5	1, 4	imbi12d 688	. . . . 5 |- (a = A -> ((R We a -> E.x e. On E.f f Isom _E , R (x, a)) <-> (R We A -> E.x e. On E.f f Isom _E , R (x, A))))
6		visset 2295	. . . . . . 7 |- a e. _V
7		rdglem1 5145	. . . . . . 7 |- {g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))} = {h | E.b e. On (h Fn b /\ A.c e. b (h` c) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (h |` c)))}
8		eqid 1884	. . . . . . 7 |- U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))} = U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}
9		breq1 3341	. . . . . . . . . . 11 |- (k = j -> (kRz <-> jRz))
10	9	cbvralv 2280	. . . . . . . . . 10 |- (A.k e. ran h kRz <-> A.j e. ran h jRz)
11	10	a1i 8	. . . . . . . . 9 |- (z e. a -> (A.k e. ran h kRz <-> A.j e. ran h jRz))
12	11	rabbiia 2285	. . . . . . . 8 |- {z e. a | A.k e. ran h kRz} = {z e. a | A.j e. ran h jRz}
13		breq2 3342	. . . . . . . . . 10 |- (z = w -> (jRz <-> jRw))
14	13	ralbidv 2123	. . . . . . . . 9 |- (z = w -> (A.j e. ran h jRz <-> A.j e. ran h jRw))
15	14	cbvrabv 2422	. . . . . . . 8 |- {z e. a | A.j e. ran h jRz} = {w e. a | A.j e. ran h jRw}
16	12, 15	eqtri 1908	. . . . . . 7 |- {z e. a | A.k e. ran h kRz} = {w e. a | A.j e. ran h jRw}
17		breq1 3341	. . . . . . . . . . 11 |- (b = j -> (bRp <-> jRp))
18	17	cbvralv 2280	. . . . . . . . . 10 |- (A.b e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)bRp <-> A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)jRp)
19	18	a1i 8	. . . . . . . . 9 |- (p e. a -> (A.b e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)bRp <-> A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)jRp))
20	19	rabbiia 2285	. . . . . . . 8 |- {p e. a | A.b e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)bRp} = {p e. a | A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)jRp}
21		breq2 3342	. . . . . . . . . 10 |- (p = w -> (jRp <-> jRw))
22	21	ralbidv 2123	. . . . . . . . 9 |- (p = w -> (A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)jRp <-> A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)jRw))
23	22	cbvrabv 2422	. . . . . . . 8 |- {p e. a | A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)jRp} = {w e. a | A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)jRw}
24	20, 23	eqtri 1908	. . . . . . 7 |- {p e. a | A.b e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)bRp} = {w e. a | A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"x)jRw}
25		breq1 3341	. . . . . . . . . . . . . . . 16 |- (m = u -> (mRn <-> uRn))
26	25	notbid 673	. . . . . . . . . . . . . . 15 |- (m = u -> (-. mRn <-> -. uRn))
27	26	cbvralv 2280	. . . . . . . . . . . . . 14 |- (A.m e. {z e. a | A.k e. ran q kRz} -. mRn <-> A.u e. {z e. a | A.k e. ran q kRz} -. uRn)
28	27	a1i 8	. . . . . . . . . . . . 13 |- (n e. {z e. a | A.k e. ran q kRz} -> (A.m e. {z e. a | A.k e. ran q kRz} -. mRn <-> A.u e. {z e. a | A.k e. ran q kRz} -. uRn))
29	28	rabbiia 2285	. . . . . . . . . . . 12 |- {n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn} = {n e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRn}
30		breq2 3342	. . . . . . . . . . . . . . 15 |- (n = v -> (uRn <-> uRv))
31	30	notbid 673	. . . . . . . . . . . . . 14 |- (n = v -> (-. uRn <-> -. uRv))
32	31	ralbidv 2123	. . . . . . . . . . . . 13 |- (n = v -> (A.u e. {z e. a | A.k e. ran q kRz} -. uRn <-> A.u e. {z e. a | A.k e. ran q kRz} -. uRv))
33	32	cbvrabv 2422	. . . . . . . . . . . 12 |- {n e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRn} = {v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv}
34	29, 33	eqtri 1908	. . . . . . . . . . 11 |- {n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn} = {v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv}
35	34	unieqi 3187	. . . . . . . . . 10 |- U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn} = U.{v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv}
36	35	eqeq2i 1894	. . . . . . . . 9 |- (o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn} <-> o = U.{v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv})
37	36	opabbii 3402	. . . . . . . 8 |- {<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}} = {<.q, o>. | o = U.{v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv}}
38		rneq 4186	. . . . . . . . . . . . . . . . . 18 |- (q = h -> ran q = ran h)
39	38	raleqdv 2269	. . . . . . . . . . . . . . . . 17 |- (q = h -> (A.k e. ran q kRz <-> A.k e. ran h kRz))
40	39	rabbidv 2287	. . . . . . . . . . . . . . . 16 |- (q = h -> {z e. a | A.k e. ran q kRz} = {z e. a | A.k e. ran h kRz})
41	40	eleq2d 1964	. . . . . . . . . . . . . . 15 |- (q = h -> (v e. {z e. a | A.k e. ran q kRz} <-> v e. {z e. a | A.k e. ran h kRz}))
42	40	raleqdv 2269	. . . . . . . . . . . . . . 15 |- (q = h -> (A.u e. {z e. a | A.k e. ran q kRz} -. uRv <-> A.u e. {z e. a | A.k e. ran h kRz} -. uRv))
43	41, 42	anbi12d 690	. . . . . . . . . . . . . 14 |- (q = h -> ((v e. {z e. a | A.k e. ran q kRz} /\ A.u e. {z e. a | A.k e. ran q kRz} -. uRv) <-> (v e. {z e. a | A.k e. ran h kRz} /\ A.u e. {z e. a | A.k e. ran h kRz} -. uRv)))
44	43	abbidv 2008	. . . . . . . . . . . . 13 |- (q = h -> {v | (v e. {z e. a | A.k e. ran q kRz} /\ A.u e. {z e. a | A.k e. ran q kRz} -. uRv)} = {v | (v e. {z e. a | A.k e. ran h kRz} /\ A.u e. {z e. a | A.k e. ran h kRz} -. uRv)})
45		df-rab 2112	. . . . . . . . . . . . 13 |- {v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv} = {v | (v e. {z e. a | A.k e. ran q kRz} /\ A.u e. {z e. a | A.k e. ran q kRz} -. uRv)}
46		df-rab 2112	. . . . . . . . . . . . 13 |- {v e. {z e. a | A.k e. ran h kRz} | A.u e. {z e. a | A.k e. ran h kRz} -. uRv} = {v | (v e. {z e. a | A.k e. ran h kRz} /\ A.u e. {z e. a | A.k e. ran h kRz} -. uRv)}
47	44, 45, 46	3eqtr4g 1953	. . . . . . . . . . . 12 |- (q = h -> {v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv} = {v e. {z e. a | A.k e. ran h kRz} | A.u e. {z e. a | A.k e. ran h kRz} -. uRv})
48	47	unieqd 3188	. . . . . . . . . . 11 |- (q = h -> U.{v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv} = U.{v e. {z e. a | A.k e. ran h kRz} | A.u e. {z e. a | A.k e. ran h kRz} -. uRv})
49	48	eqeq2d 1895	. . . . . . . . . 10 |- (q = h -> (o = U.{v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv} <-> o = U.{v e. {z e. a | A.k e. ran h kRz} | A.u e. {z e. a | A.k e. ran h kRz} -. uRv}))
50		eqeq1 1890	. . . . . . . . . 10 |- (o = c -> (o = U.{v e. {z e. a | A.k e. ran h kRz} | A.u e. {z e. a | A.k e. ran h kRz} -. uRv} <-> c = U.{v e. {z e. a | A.k e. ran h kRz} | A.u e. {z e. a | A.k e. ran h kRz} -. uRv}))
51	49, 50	sylan9bb 599	. . . . . . . . 9 |- ((q = h /\ o = c) -> (o = U.{v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv} <-> c = U.{v e. {z e. a | A.k e. ran h kRz} | A.u e. {z e. a | A.k e. ran h kRz} -. uRv}))
52	51	cbvopabv 3404	. . . . . . . 8 |- {<.q, o>. | o = U.{v e. {z e. a | A.k e. ran q kRz} | A.u e. {z e. a | A.k e. ran q kRz} -. uRv}} = {<.h, c>. | c = U.{v e. {z e. a | A.k e. ran h kRz} | A.u e. {z e. a | A.k e. ran h kRz} -. uRv}}
53	37, 52	eqtri 1908	. . . . . . 7 |- {<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}} = {<.h, c>. | c = U.{v e. {z e. a | A.k e. ran h kRz} | A.u e. {z e. a | A.k e. ran h kRz} -. uRv}}
54	17	cbvralv 2280	. . . . . . . . . 10 |- (A.b e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)bRp <-> A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)jRp)
55	54	a1i 8	. . . . . . . . 9 |- (p e. a -> (A.b e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)bRp <-> A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)jRp))
56	55	rabbiia 2285	. . . . . . . 8 |- {p e. a | A.b e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)bRp} = {p e. a | A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)jRp}
57	21	ralbidv 2123	. . . . . . . . 9 |- (p = w -> (A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)jRp <-> A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)jRw))
58	57	cbvrabv 2422	. . . . . . . 8 |- {p e. a | A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)jRp} = {w e. a | A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)jRw}
59	56, 58	eqtri 1908	. . . . . . 7 |- {p e. a | A.b e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)bRp} = {w e. a | A.j e. (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}"y)jRw}
60	6, 7, 8, 16, 24, 53, 59	ordtypelem7 5690	. . . . . 6 |- (R We a -> E.x e. On (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))} |` x) Isom _E , R (x, a))
61	7, 8	tfrlem7 5125	. . . . . . . . 9 |- Fun U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))}
62		visset 2295	. . . . . . . . 9 |- x e. _V
63		resfunexg 4500	. . . . . . . . 9 |- ((Fun U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))} /\ x e. _V) -> (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))} |` x) e. _V)
64	61, 62, 63	mp2an 761	. . . . . . . 8 |- (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))} |` x) e. _V
65		isoeq1 4863	. . . . . . . 8 |- (f = (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))} |` x) -> (f Isom _E , R (x, a) <-> (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))} |` x) Isom _E , R (x, a)))
66	64, 65	cla4ev 2371	. . . . . . 7 |- ((U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))} |` x) Isom _E , R (x, a) -> E.f f Isom _E , R (x, a))
67	66	reximi 2198	. . . . . 6 |- (E.x e. On (U.{g | E.r e. On (g Fn r /\ A.s e. r (g` s) = ({<.q, o>. | o = U.{n e. {z e. a | A.k e. ran q kRz} | A.m e. {z e. a | A.k e. ran q kRz} -. mRn}}` (g |` s)))} |` x) Isom _E , R (x, a) -> E.x e. On E.f f Isom _E , R (x, a))
68	60, 67	syl 12	. . . . 5 |- (R We a -> E.x e. On E.f f Isom _E , R (x, a))
69	5, 68	vtoclg 2346	. . . 4 |- (A e. B -> (R We A -> E.x e. On E.f f Isom _E , R (x, A)))
70	69	imp 377	. . 3 |- ((A e. B /\ R We A) -> E.x e. On E.f f Isom _E , R (x, A))
71		hbe1 1363	. . . . . . . 8 |- (E.f f Isom _E , R (y, A) -> A.fE.f f Isom _E , R (y, A))
72		ax-17 1317	. . . . . . . 8 |- (((x e. On /\ y e. On) -> x = y) -> A.f((x e. On /\ y e. On) -> x = y))
73	71, 72	hbim 1354	. . . . . . 7 |- ((E.f f Isom _E , R (y, A) -> ((x e. On /\ y e. On) -> x = y)) -> A.f(E.f f Isom _E , R (y, A) -> ((x e. On /\ y e. On) -> x = y)))
74		ordiso 5683	. . . . . . . . . . . . 13 |- ((x e. On /\ y e. On) -> (x = y <-> E.h h Isom _E , _E (x, y)))
75		visset 2295	. . . . . . . . . . . . . . . 16 |- g e. _V
76	75	cnvex 4425	. . . . . . . . . . . . . . 15 |- `'g e. _V
77		visset 2295	. . . . . . . . . . . . . . 15 |- f e. _V
78	76, 77	coex 4430	. . . . . . . . . . . . . 14 |- (`'g o. f) e. _V
79		isoeq1 4863	. . . . . . . . . . . . . 14 |- (h = (`'g o. f) -> (h Isom _E , _E (x, y) <-> (`'g o. f) Isom _E , _E (x, y)))
80	78, 79	cla4ev 2371	. . . . . . . . . . . . 13 |- ((`'g o. f) Isom _E , _E (x, y) -> E.h h Isom _E , _E (x, y))
81	74, 80	syl5bir 227	. . . . . . . . . . . 12 |- ((x e. On /\ y e. On) -> ((`'g o. f) Isom _E , _E (x, y) -> x = y))
82		isotr 4874	. . . . . . . . . . . 12 |- ((f Isom _E , R (x, A) /\ `'g Isom R, _E (A, y)) -> (`'g o. f) Isom _E , _E (x, y))
83	81, 82	syl5com 63	. . . . . . . . . . 11 |- ((f Isom _E , R (x, A) /\ `'g Isom R, _E (A, y)) -> ((x e. On /\ y e. On) -> x = y))
84	83	ex 402	. . . . . . . . . 10 |- (f Isom _E , R (x, A) -> (`'g Isom R, _E (A, y) -> ((x e. On /\ y e. On) -> x = y)))
85		isocnv 4873	. . . . . . . . . 10 |- (g Isom _E , R (y, A) -> `'g Isom R, _E (A, y))
86	84, 85	syl5 20	. . . . . . . . 9 |- (f Isom _E , R (x, A) -> (g Isom _E , R (y, A) -> ((x e. On /\ y e. On) -> x = y)))
87	86	19.23adv 1584	. . . . . . . 8 |- (f Isom _E , R (x, A) -> (E.g g Isom _E , R (y, A) -> ((x e. On /\ y e. On) -> x = y)))
88		isoeq1 4863	. . . . . . . . 9 |- (f = g -> (f Isom _E , R (y, A) <-> g Isom _E , R (y, A)))
89	88	cbvexv 1697	. . . . . . . 8 |- (E.f f Isom _E , R (y, A) <-> E.g g Isom _E , R (y, A))
90	87, 89	syl5ib 223	. . . . . . 7 |- (f Isom _E , R (x, A) -> (E.f f Isom _E , R (y, A) -> ((x e. On /\ y e. On) -> x = y)))
91	73, 90	19.23ai 1412	. . . . . 6 |- (E.f f Isom _E , R (x, A) -> (E.f f Isom _E , R (y, A) -> ((x e. On /\ y e. On) -> x = y)))
92	91	imp 377	. . . . 5 |- ((E.f f Isom _E , R (x, A) /\ E.f f Isom _E , R (y, A)) -> ((x e. On /\ y e. On) -> x = y))
93	92	com12 14	. . . 4 |- ((x e. On /\ y e. On) -> ((E.f f Isom _E , R (x, A) /\ E.f f Isom _E , R (y, A)) -> x = y))
94	93	rgen2a 2160	. . 3 |- A.x e. On A.y e. On ((E.f f Isom _E , R (x, A) /\ E.f f Isom _E , R (y, A)) -> x = y)
95	70, 94	jctir 317	. 2 |- ((A e. B /\ R We A) -> (E.x e. On E.f f Isom _E , R (x, A) /\ A.x e. On A.y e. On ((E.f f Isom _E , R (x, A) /\ E.f f Isom _E , R (y, A)) -> x = y)))
96		isoeq4 4866	. . . 4 |- (x = y -> (f Isom _E , R (x, A) <-> f Isom _E , R (y, A)))
97	96	exbidv 1657	. . 3 |- (x = y -> (E.f f Isom _E , R (x, A) <-> E.f f Isom _E , R (y, A)))
98	97	reu4 2446	. 2 |- (E!x e. On E.f f Isom _E , R (x, A) <-> (E.x e. On E.f f Isom _E , R (x, A) /\ A.x e. On A.y e. On ((E.f f Isom _E , R (x, A) /\ E.f f Isom _E , R (y, A)) -> x = y)))
99	95, 98	sylibr 217	1 |- ((A e. B /\ R We A) -> E!x e. On E.f f Isom _E , R (x, A))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  A.wral 2105  E.wrex 2106  E!wreu 2107  {crab 2108  _Vcvv 2292  U.cuni 3177   class class class wbr 3338  {copab 3395   _E cep 3581   We wwe 3624  Oncon0 3657  `'ccnv 3985  ran crn 3987   |` cres 3988  "cima 3989   o. ccom 3990  Fun wfun 3992   Fn wfn 3993  ` cfv 3998   Isom wiso 3999

This theorem is referenced by:  hartog 5693  hartogOLD 15384

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-suc 3663  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-iso 4015

Copyright terms: Public domain