Theorem hartoglemOLD 15383

Description: Lemma for hartog 5693. (Moved to hartoglem 5692 in main set.mm and may be deleted by mathbox owner, JGH. --NM 26-Aug-2011.)

Hypotheses

Ref	Expression
hartog.1OLD	|- H = {x e. On | x ~<_ A}
hartoglem.2OLD	|- R = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}

Assertion

Ref	Expression
hartoglemOLD	|- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> g Isom _E , R (t, (g"t)))

Distinct variable groups:   a,b,c,d,g,t,x,A   B,a,b,c,d,g,t   H,a,b,c,d,g,t

Proof of Theorem hartoglemOLD

Step	Hyp	Ref	Expression
1		df-iso 4015	. 2 |- (g Isom _E , R (t, (g"t)) <-> (g:t-1-1-onto->(g"t) /\ A.r e. t A.s e. t (r _E s <-> (g` r)R(g` s))))
2		df-f1o 4013	. . . 4 |- (g:t-1-1-onto->(g"t) <-> (g:t-1-1->(g"t) /\ g:t-onto->(g"t)))
3		df-f1 4011	. . . . 5 |- (g:t-1-1->(g"t) <-> (g:t-->(g"t) /\ Fun `'g))
4		f1f 4610	. . . . . . 7 |- (g:t-1-1->A -> g:t-->A)
5		ffn 4562	. . . . . . 7 |- (g:t-->A -> g Fn t)
6		dffn4 4623	. . . . . . . 8 |- (g Fn t <-> g:t-onto->ran g)
7		fof 4617	. . . . . . . 8 |- (g:t-onto->ran g -> g:t-->ran g)
8	6, 7	sylbi 216	. . . . . . 7 |- (g Fn t -> g:t-->ran g)
9	4, 5, 8	3syl 24	. . . . . 6 |- (g:t-1-1->A -> g:t-->ran g)
10		fnima 4530	. . . . . . . 8 |- (g Fn t -> (g"t) = ran g)
11	4, 5, 10	3syl 24	. . . . . . 7 |- (g:t-1-1->A -> (g"t) = ran g)
12		feq3 4553	. . . . . . 7 |- ((g"t) = ran g -> (g:t-->(g"t) <-> g:t-->ran g))
13	11, 12	syl 12	. . . . . 6 |- (g:t-1-1->A -> (g:t-->(g"t) <-> g:t-->ran g))
14	9, 13	mpbird 213	. . . . 5 |- (g:t-1-1->A -> g:t-->(g"t))
15		df-f1 4011	. . . . . 6 |- (g:t-1-1->A <-> (g:t-->A /\ Fun `'g))
16	15	simprbi 353	. . . . 5 |- (g:t-1-1->A -> Fun `'g)
17	3, 14, 16	sylanbrc 527	. . . 4 |- (g:t-1-1->A -> g:t-1-1->(g"t))
18		df-fo 4012	. . . . 5 |- (g:t-onto->(g"t) <-> (g Fn t /\ ran g = (g"t)))
19	4, 5	syl 12	. . . . 5 |- (g:t-1-1->A -> g Fn t)
20	11	eqcomd 1889	. . . . 5 |- (g:t-1-1->A -> ran g = (g"t))
21	18, 19, 20	sylanbrc 527	. . . 4 |- (g:t-1-1->A -> g:t-onto->(g"t))
22	2, 17, 21	sylanbrc 527	. . 3 |- (g:t-1-1->A -> g:t-1-1-onto->(g"t))
23	22	ad2antlr 441	. 2 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> g:t-1-1-onto->(g"t))
24		simprll 456	. . . . . . . 8 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((r e. t /\ s e. t) /\ r e. s)) -> r e. t)
25		simprlr 457	. . . . . . . 8 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((r e. t /\ s e. t) /\ r e. s)) -> s e. t)
26		eqidd 1885	. . . . . . . 8 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((r e. t /\ s e. t) /\ r e. s)) -> (g` r) = (g` r))
27		eqidd 1885	. . . . . . . 8 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((r e. t /\ s e. t) /\ r e. s)) -> (g` s) = (g` s))
28		simprr 451	. . . . . . . 8 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((r e. t /\ s e. t) /\ r e. s)) -> r e. s)
29		fveq2 4681	. . . . . . . . . . 11 |- (c = r -> (g` c) = (g` r))
30	29	eqeq2d 1895	. . . . . . . . . 10 |- (c = r -> ((g` r) = (g` c) <-> (g` r) = (g` r)))
31		eleq1 1957	. . . . . . . . . 10 |- (c = r -> (c e. d <-> r e. d))
32	30, 31	3anbi13d 1170	. . . . . . . . 9 |- (c = r -> (((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d) <-> ((g` r) = (g` r) /\ (g` s) = (g` d) /\ r e. d)))
33		fveq2 4681	. . . . . . . . . . 11 |- (d = s -> (g` d) = (g` s))
34	33	eqeq2d 1895	. . . . . . . . . 10 |- (d = s -> ((g` s) = (g` d) <-> (g` s) = (g` s)))
35		eleq2 1958	. . . . . . . . . 10 |- (d = s -> (r e. d <-> r e. s))
36	34, 35	3anbi23d 1171	. . . . . . . . 9 |- (d = s -> (((g` r) = (g` r) /\ (g` s) = (g` d) /\ r e. d) <-> ((g` r) = (g` r) /\ (g` s) = (g` s) /\ r e. s)))
37	32, 36	rcla42ev 2385	. . . . . . . 8 |- ((r e. t /\ s e. t /\ ((g` r) = (g` r) /\ (g` s) = (g` s) /\ r e. s)) -> E.c e. t E.d e. t ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))
38	24, 25, 26, 27, 28, 37	syl113anc 1112	. . . . . . 7 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((r e. t /\ s e. t) /\ r e. s)) -> E.c e. t E.d e. t ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))
39	38	expr 418	. . . . . 6 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) -> (r e. s -> E.c e. t E.d e. t ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d)))
40		simprr3 926	. . . . . . . . 9 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> c e. d)
41		simprr1 924	. . . . . . . . . . 11 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> (g` r) = (g` c))
42		simplr 449	. . . . . . . . . . . . 13 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> g:t-1-1->A)
43	42	ad2antrr 440	. . . . . . . . . . . 12 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> g:t-1-1->A)
44		simplrl 454	. . . . . . . . . . . 12 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> r e. t)
45		simprll 456	. . . . . . . . . . . 12 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> c e. t)
46		f1fveq 4852	. . . . . . . . . . . 12 |- ((g:t-1-1->A /\ (r e. t /\ c e. t)) -> ((g` r) = (g` c) <-> r = c))
47	43, 44, 45, 46	syl12anc 1098	. . . . . . . . . . 11 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> ((g` r) = (g` c) <-> r = c))
48	41, 47	mpbid 212	. . . . . . . . . 10 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> r = c)
49		simprr2 925	. . . . . . . . . . 11 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> (g` s) = (g` d))
50		simplrr 455	. . . . . . . . . . . 12 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> s e. t)
51		simprlr 457	. . . . . . . . . . . 12 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> d e. t)
52		f1fveq 4852	. . . . . . . . . . . 12 |- ((g:t-1-1->A /\ (s e. t /\ d e. t)) -> ((g` s) = (g` d) <-> s = d))
53	43, 50, 51, 52	syl12anc 1098	. . . . . . . . . . 11 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> ((g` s) = (g` d) <-> s = d))
54	49, 53	mpbid 212	. . . . . . . . . 10 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> s = d)
55	48, 54	eleq12d 1965	. . . . . . . . 9 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> (r e. s <-> c e. d))
56	40, 55	mpbird 213	. . . . . . . 8 |- (((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) /\ ((c e. t /\ d e. t) /\ ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))) -> r e. s)
57	56	exp32 408	. . . . . . 7 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) -> ((c e. t /\ d e. t) -> (((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d) -> r e. s)))
58	57	r19.23advv 2218	. . . . . 6 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) -> (E.c e. t E.d e. t ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d) -> r e. s))
59	39, 58	impbid 574	. . . . 5 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) -> (r e. s <-> E.c e. t E.d e. t ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d)))
60		epel 3585	. . . . 5 |- (r _E s <-> r e. s)
61		fvex 4689	. . . . . 6 |- (g` r) e. _V
62		fvex 4689	. . . . . 6 |- (g` s) e. _V
63		eqeq1 1890	. . . . . . . 8 |- (a = (g` r) -> (a = (g` c) <-> (g` r) = (g` c)))
64	63	3anbi1d 1172	. . . . . . 7 |- (a = (g` r) -> ((a = (g` c) /\ b = (g` d) /\ c e. d) <-> ((g` r) = (g` c) /\ b = (g` d) /\ c e. d)))
65	64	2rexbidv 2141	. . . . . 6 |- (a = (g` r) -> (E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d) <-> E.c e. t E.d e. t ((g` r) = (g` c) /\ b = (g` d) /\ c e. d)))
66		eqeq1 1890	. . . . . . . 8 |- (b = (g` s) -> (b = (g` d) <-> (g` s) = (g` d)))
67	66	3anbi2d 1173	. . . . . . 7 |- (b = (g` s) -> (((g` r) = (g` c) /\ b = (g` d) /\ c e. d) <-> ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d)))
68	67	2rexbidv 2141	. . . . . 6 |- (b = (g` s) -> (E.c e. t E.d e. t ((g` r) = (g` c) /\ b = (g` d) /\ c e. d) <-> E.c e. t E.d e. t ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d)))
69		hartoglem.2OLD	. . . . . 6 |- R = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}
70	61, 62, 65, 68, 69	brab 3571	. . . . 5 |- ((g` r)R(g` s) <-> E.c e. t E.d e. t ((g` r) = (g` c) /\ (g` s) = (g` d) /\ c e. d))
71	59, 60, 70	3bitr4g 614	. . . 4 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (r e. t /\ s e. t)) -> (r _E s <-> (g` r)R(g` s)))
72	71	ex 402	. . 3 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> ((r e. t /\ s e. t) -> (r _E s <-> (g` r)R(g` s))))
73	72	r19.21aivv 2183	. 2 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> A.r e. t A.s e. t (r _E s <-> (g` r)R(g` s)))
74	1, 23, 73	sylanbrc 527	1 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> g Isom _E , R (t, (g"t)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  {crab 2108   class class class wbr 3338  {copab 3395   _E cep 3581  Oncon0 3657  `'ccnv 3985  ran crn 3987  "cima 3989  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998   Isom wiso 3999   ~<_ cdom 5424

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-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-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-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-eprel 3583  df-id 3586  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