Theorem aceq5lem2 4736

Description: Lemma for aceq5 4740.

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 2511	. . 3 |- U.A = U.{u | (u =/= (/) /\ E.t e. h u = ({t} X. t))}
3	2	eleq2i 1538	. 2 |- (<.w, g>. e. U.A <-> <.w, g>. e. U.{u | (u =/= (/) /\ E.t e. h u = ({t} X. t))})
4		eluniab 2513	. . 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 1764	. . . . 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 1051	. . 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 1824	. . . 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 1650	. . . 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 2286	. . . . . . . . . . 11 |- (<.w, g>. e. u -> u =/= (/))
15	14	pm4.71i 637	. . . . . . . . . 10 |- (<.w, g>. e. u <-> (<.w, g>. e. u /\ u =/= (/)))
16	15	anbi2i 480	. . . . . . . . 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 1051	. . . . . . 7 |- (E.u((<.w, g>. e. u /\ u =/= (/)) /\ u = ({t} X. t)) <-> E.u(u = ({t} X. t) /\ <.w, g>. e. u))
19		snex 2750	. . . . . . . . 9 |- {t} e. V
20		visset 1813	. . . . . . . . 9 |- t e. V
21	19, 20	xpex 3260	. . . . . . . 8 |- ({t} X. t) e. V
22		eleq2 1535	. . . . . . . 8 |- (u = ({t} X. t) -> (<.w, g>. e. u <-> <.w, g>. e. ({t} X. t)))
23	21, 22	ceqsexv 1835	. . . . . . 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 480	. . . . 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 1813	. . . . . . . 8 |- g e. V
27	26	opelxp 3214	. . . . . . 7 |- (<.w, g>. e. ({t} X. t) <-> (w e. {t} /\ g e. t))
28		elsn 2421	. . . . . . . . 9 |- (w e. {t} <-> w = t)
29		eqcom 1477	. . . . . . . . 9 |- (w = t <-> t = w)
30	28, 29	bitr 173	. . . . . . . 8 |- (w e. {t} <-> t = w)
31	30	anbi1i 481	. . . . . . 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 480	. . . . 5 |- ((t e. h /\ <.w, g>. e. ({t} X. t)) <-> (t e. h /\ (t = w /\ g e. t)))
34		an12 484	. . . . 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 1051	. . 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 1813	. . . 4 |- w e. V
38		eleq1 1534	. . . . 5 |- (t = w -> (t e. h <-> w e. h))
39		eleq2 1535	. . . . 5 |- (t = w -> (g e. t <-> g e. w))
40	38, 39	anbi12d 628	. . . 4 |- (t = w -> ((t e. h /\ g e. t) <-> (w e. h /\ g e. w)))
41	37, 40	ceqsexv 1835	. . 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 956   e. wcel 958  E.wex 980  {cab 1463   =/= wne 1585  E.wrex 1646  (/)c0 2280  {csn 2409  <.cop 2411  U.cuni 2503   X. cxp 3168

This theorem is referenced by:  aceq5lem5 4739

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-opab 2667  df-xp 3184  df-rel 3185

Copyright terms: Public domain