Theorem aceq5lem2 4708

Description: Lemma for aceq5 4712.

Hypothesis

Ref	Expression
aceq5lem.1	|- A = {u | (u =/= (/) /\ E.t e. h u = ({t} X. t))}

Assertion

Ref	Expression
aceq5lem2	|- (<.w, g>. e. U.A <-> (w e. h /\ g e. w))

Distinct variable groups:   w,u,t,h,g   w,A,g

Proof of Theorem aceq5lem2

Step	Hyp	Ref	Expression
1		aceq5lem.1	. . . 4 |- A = {u | (u =/= (/) /\ E.t e. h u = ({t} X. t))}
2	1	unieqi 2501	. . 3 |- U.A = U.{u | (u =/= (/) /\ E.t e. h u = ({t} X. t))}
3	2	eleq2i 1530	. 2 |- (<.w, g>. e. U.A <-> <.w, g>. e. U.{u | (u =/= (/) /\ E.t e. h u = ({t} X. t))})
4		eluniab 2503	. . 3 |- (<.w, g>. e. U.{u | (u =/= (/) /\ E.t e. h u = ({t} X. t))} <-> E.u(<.w, g>. e. u /\ (u =/= (/) /\ E.t e. h u = ({t} X. t))))
5		r19.42v 1756	. . . . 5 |- (E.t e. h ((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)) <-> ((<.w, g>. e. u /\ u =/= (/)) /\ E.t e. h u = ({t} X. t)))
6		anass 439	. . . . 5 |- (((<.w, g>. e. u /\ u =/= (/)) /\ E.t e. h u = ({t} X. t)) <-> (<.w, g>. e. u /\ (u =/= (/) /\ E.t e. h u = ({t} X. t))))
7	5, 6	bitr2 174	. . . 4 |- ((<.w, g>. e. u /\ (u =/= (/) /\ E.t e. h u = ({t} X. t))) <-> E.t e. h ((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)))
8	7	exbii 1047	. . 3 |- (E.u(<.w, g>. e. u /\ (u =/= (/) /\ E.t e. h u = ({t} X. t))) <-> E.uE.t e. h ((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)))
9		rexcom4 1815	. . . 4 |- (E.t e. h E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)) <-> E.uE.t e. h ((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)))
10		df-rex 1642	. . . 4 |- (E.t e. h E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)) <-> E.t(t e. h /\ E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t))))
11	9, 10	bitr3 175	. . 3 |- (E.uE.t e. h ((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)) <-> E.t(t e. h /\ E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t))))
12	4, 8, 11	3bitr 177	. 2 |- (<.w, g>. e. U.{u | (u =/= (/) /\ E.t e. h u = ({t} X. t))} <-> E.t(t e. h /\ E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t))))
13		ancom 435	. . . . . . . . 9 |- (((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)) <-> (u = ({t} X. t) /\ (<.w, g>. e. u /\ u =/= (/))))
14		ne0i 2276	. . . . . . . . . . 11 |- (<.w, g>. e. u -> u =/= (/))
15	14	pm4.71i 635	. . . . . . . . . 10 |- (<.w, g>. e. u <-> (<.w, g>. e. u /\ u =/= (/)))
16	15	anbi2i 479	. . . . . . . . 9 |- ((u = ({t} X. t) /\ <.w, g>. e. u) <-> (u = ({t} X. t) /\ (<.w, g>. e. u /\ u =/= (/))))
17	13, 16	bitr4 176	. . . . . . . 8 |- (((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)) <-> (u = ({t} X. t) /\ <.w, g>. e. u))
18	17	exbii 1047	. . . . . . 7 |- (E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)) <-> E.u(u = ({t} X. t) /\ <.w, g>. e. u))
19		snex 2740	. . . . . . . . 9 |- {t} e. V
20		visset 1804	. . . . . . . . 9 |- t e. V
21	19, 20	xpex 3250	. . . . . . . 8 |- ({t} X. t) e. V
22		eleq2 1527	. . . . . . . 8 |- (u = ({t} X. t) -> (<.w, g>. e. u <-> <.w, g>. e. ({t} X. t)))
23	21, 22	ceqsexv 1826	. . . . . . 7 |- (E.u(u = ({t} X. t) /\ <.w, g>. e. u) <-> <.w, g>. e. ({t} X. t))
24	18, 23	bitr 173	. . . . . 6 |- (E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)) <-> <.w, g>. e. ({t} X. t))
25	24	anbi2i 479	. . . . 5 |- ((t e. h /\ E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t))) <-> (t e. h /\ <.w, g>. e. ({t} X. t)))
26		visset 1804	. . . . . . . 8 |- g e. V
27	26	opelxp 3204	. . . . . . 7 |- (<.w, g>. e. ({t} X. t) <-> (w e. {t} /\ g e. t))
28		elsn 2411	. . . . . . . . 9 |- (w e. {t} <-> w = t)
29		eqcom 1469	. . . . . . . . 9 |- (w = t <-> t = w)
30	28, 29	bitr 173	. . . . . . . 8 |- (w e. {t} <-> t = w)
31	30	anbi1i 480	. . . . . . 7 |- ((w e. {t} /\ g e. t) <-> (t = w /\ g e. t))
32	27, 31	bitr 173	. . . . . 6 |- (<.w, g>. e. ({t} X. t) <-> (t = w /\ g e. t))
33	32	anbi2i 479	. . . . 5 |- ((t e. h /\ <.w, g>. e. ({t} X. t)) <-> (t e. h /\ (t = w /\ g e. t)))
34		an12 483	. . . . 5 |- ((t e. h /\ (t = w /\ g e. t)) <-> (t = w /\ (t e. h /\ g e. t)))
35	25, 33, 34	3bitr 177	. . . 4 |- ((t e. h /\ E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t))) <-> (t = w /\ (t e. h /\ g e. t)))
36	35	exbii 1047	. . 3 |- (E.t(t e. h /\ E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t))) <-> E.t(t = w /\ (t e. h /\ g e. t)))
37		visset 1804	. . . 4 |- w e. V
38		eleq1 1526	. . . . 5 |- (t = w -> (t e. h <-> w e. h))
39		eleq2 1527	. . . . 5 |- (t = w -> (g e. t <-> g e. w))
40	38, 39	anbi12d 626	. . . 4 |- (t = w -> ((t e. h /\ g e. t) <-> (w e. h /\ g e. w)))
41	37, 40	ceqsexv 1826	. . 3 |- (E.t(t = w /\ (t e. h /\ g e. t)) <-> (w e. h /\ g e. w))
42	36, 41	bitr 173	. 2 |- (E.t(t e. h /\ E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t))) <-> (w e. h /\ g e. w))
43	3, 12, 42	3bitr 177	1 |- (<.w, g>. e. U.A <-> (w e. h /\ g e. w))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977  {cab 1456   =/= wne 1577  E.wrex 1638  (/)c0 2270  {csn 2399  <.cop 2401  U.cuni 2493   X. cxp 3158

This theorem is referenced by:  aceq5lem5 4711

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-opab 2657  df-xp 3174  df-rel 3175

Copyright terms: Public domain