Theorem aceq5lem3 3560

Description: Lemma for aceq5 3563.

Hypothesis

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

Assertion

Ref	Expression
aceq5lem3	|- (({w} X. w) e. A <-> (-. w = (/) /\ w e. h))

Distinct variable group(s):   w,u,t,h   w,A

Proof of Theorem aceq5lem3

Step	Hyp	Ref	Expression
1		snex 1859	. . . 4 |- {w} e. V
2		visset 1350	. . . 4 |- w e. V
3	1, 2	xpex 2488	. . 3 |- ({w} X. w) e. V
4		cleq1 1107	. . . . 5 |- (u = ({w} X. w) -> (u = (/) <-> ({w} X. w) = (/)))
5	4	negbid 463	. . . 4 |- (u = ({w} X. w) -> (-. u = (/) <-> -. ({w} X. w) = (/)))
6		cleq1 1107	. . . . 5 |- (u = ({w} X. w) -> (u = ({t} X. t) <-> ({w} X. w) = ({t} X. t)))
7	6	birexdv 1220	. . . 4 |- (u = ({w} X. w) -> (E.t e. h u = ({t} X. t) <-> E.t e. h ({w} X. w) = ({t} X. t)))
8	5, 7	anbi12d 476	. . 3 |- (u = ({w} X. w) -> ((-. u = (/) /\ E.t e. h u = ({t} X. t)) <-> (-. ({w} X. w) = (/) /\ E.t e. h ({w} X. w) = ({t} X. t))))
9	3, 8	elab 1415	. 2 |- (({w} X. w) e. {u | (-. u = (/) /\ E.t e. h u = ({t} X. t))} <-> (-. ({w} X. w) = (/) /\ E.t e. h ({w} X. w) = ({t} X. t)))
10		aceq5lem.1	. . 3 |- A = {u | (-. u = (/) /\ E.t e. h u = ({t} X. t))}
11	10	eleq2i 1153	. 2 |- (({w} X. w) e. A <-> ({w} X. w) e. {u | (-. u = (/) /\ E.t e. h u = ({t} X. t))})
12		xpeq2 2441	. . . . . 6 |- (w = (/) -> ({w} X. w) = ({w} X. (/)))
13		xp0 2652	. . . . . 6 |- ({w} X. (/)) = (/)
14	12, 13	syl6eq 1140	. . . . 5 |- (w = (/) -> ({w} X. w) = (/))
15		rneq 2555	. . . . . 6 |- (({w} X. w) = (/) -> ran ({w} X. w) = ran (/))
16	2	snnz 1846	. . . . . . 7 |- -. {w} = (/)
17		rnxp 2657	. . . . . . 7 |- (-. {w} = (/) -> ran ({w} X. w) = w)
18	16, 17	ax-mp 6	. . . . . 6 |- ran ({w} X. w) = w
19		rn0 2567	. . . . . 6 |- ran (/) = (/)
20	15, 18, 19	3eqtr3g 1146	. . . . 5 |- (({w} X. w) = (/) -> w = (/))
21	14, 20	impbi 139	. . . 4 |- (w = (/) <-> ({w} X. w) = (/))
22	21	negbii 162	. . 3 |- (-. w = (/) <-> -. ({w} X. w) = (/))
23		rneq 2555	. . . . . . . . . . 11 |- (({w} X. w) = ({t} X. t) -> ran ({w} X. w) = ran ({t} X. t))
24		visset 1350	. . . . . . . . . . . . 13 |- t e. V
25	24	snnz 1846	. . . . . . . . . . . 12 |- -. {t} = (/)
26		rnxp 2657	. . . . . . . . . . . 12 |- (-. {t} = (/) -> ran ({t} X. t) = t)
27	25, 26	ax-mp 6	. . . . . . . . . . 11 |- ran ({t} X. t) = t
28	23, 18, 27	3eqtr3g 1146	. . . . . . . . . 10 |- (({w} X. w) = ({t} X. t) -> w = t)
29		sneq 1816	. . . . . . . . . . . 12 |- (w = t -> {w} = {t})
30		xpeq1 2440	. . . . . . . . . . . 12 |- ({w} = {t} -> ({w} X. w) = ({t} X. w))
31	29, 30	syl 12	. . . . . . . . . . 11 |- (w = t -> ({w} X. w) = ({t} X. w))
32		xpeq2 2441	. . . . . . . . . . 11 |- (w = t -> ({t} X. w) = ({t} X. t))
33	31, 32	eqtrd 1128	. . . . . . . . . 10 |- (w = t -> ({w} X. w) = ({t} X. t))
34	28, 33	impbi 139	. . . . . . . . 9 |- (({w} X. w) = ({t} X. t) <-> w = t)
35		cleqcom 1103	. . . . . . . . 9 |- (w = t <-> t = w)
36	34, 35	bitr 151	. . . . . . . 8 |- (({w} X. w) = ({t} X. t) <-> t = w)
37	36	anbi2i 367	. . . . . . 7 |- ((t e. h /\ ({w} X. w) = ({t} X. t)) <-> (t e. h /\ t = w))
38		ancom 333	. . . . . . 7 |- ((t e. h /\ t = w) <-> (t = w /\ t e. h))
39	37, 38	bitr 151	. . . . . 6 |- ((t e. h /\ ({w} X. w) = ({t} X. t)) <-> (t = w /\ t e. h))
40	39	biex 733	. . . . 5 |- (E.t(t e. h /\ ({w} X. w) = ({t} X. t)) <-> E.t(t = w /\ t e. h))
41		eleq1 1149	. . . . . 6 |- (t = w -> (t e. h <-> w e. h))
42	2, 41	ceqsexv 1371	. . . . 5 |- (E.t(t = w /\ t e. h) <-> w e. h)
43	40, 42	bitr2 152	. . . 4 |- (w e. h <-> E.t(t e. h /\ ({w} X. w) = ({t} X. t)))
44		df-rex 1206	. . . 4 |- (E.t e. h ({w} X. w) = ({t} X. t) <-> E.t(t e. h /\ ({w} X. w) = ({t} X. t)))
45	43, 44	bitr4 154	. . 3 |- (w e. h <-> E.t e. h ({w} X. w) = ({t} X. t))
46	22, 45	anbi12i 369	. 2 |- ((-. w = (/) /\ w e. h) <-> (-. ({w} X. w) = (/) /\ E.t e. h ({w} X. w) = ({t} X. t)))
47	9, 11, 46	3bitr4 158	1 |- (({w} X. w) e. A <-> (-. w = (/) /\ w e. h))

Syntax hints:  -. wn 1   <-> wb 127   /\ wa 196  E.wex 678   = weq 797   e. wel 803  {cab 1090   = wceq 1091   e. wcel 1092  E.wrex 1202  (/)c0 1707  {csn 1808   X. cxp 2408  ran crn 2411

This theorem is referenced by:  aceq5lem5 3562

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-rel 2425  df-cnv 2426  df-dm 2428  df-rn 2429

metamath.org