Theorem abfii4OLD 4564

Description: Two ways to express the collection of finite intersections of a set A. Even though the expressions differ by only one symbol, the proof is not simple.

Hypothesis

Ref	Expression
abfii2x.1	|- A e. V

Assertion

Ref	Expression
abfii4OLD	|- |^|{x | (A (_ x /\ A.y((y (_ x /\ y =/= (/) /\ E.z e. om y ~~ z) -> |^|y e. x))} = |^|{x | (A (_ x /\ A.y((y (_ A /\ y =/= (/) /\ E.z e. om y ~~ z) -> |^|y e. x))}

Distinct variable group:   x,y,z,A

Proof of Theorem abfii4OLD

Step	Hyp	Ref	Expression
1		abfii2x.1	. . . . . . 7 |- A e. V
2		df-sn 2412	. . . . . . . 8 |- {|^|v} = {w | w = |^|v}
3		snex 2750	. . . . . . . 8 |- {|^|v} e. V
4	2, 3	eqeltrr 1545	. . . . . . 7 |- {w | w = |^|v} e. V
5	1, 4	abexssex 3872	. . . . . 6 |- {w | E.v(v (_ A /\ w = |^|v)} e. V
6		3simpb 786	. . . . . . . 8 |- ((v (_ A /\ E.u e. om v ~~ u /\ w = |^|v) -> (v (_ A /\ w = |^|v))
7	6	19.22i 1040	. . . . . . 7 |- (E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v) -> E.v(v (_ A /\ w = |^|v))
8	7	ss2abi 2120	. . . . . 6 |- {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} (_ {w | E.v(v (_ A /\ w = |^|v)}
9	5, 8	ssexi 2720	. . . . 5 |- {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} e. V
10		sseq2 2083	. . . . . . 7 |- (x = {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} -> (A (_ x <-> A (_ {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)}))
11		sseq2 2083	. . . . . . . . . 10 |- (x = {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} -> (y (_ x <-> y (_ {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)}))
12	11	3anbi1d 897	. . . . . . . . 9 |- (x = {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} -> ((y (_ x /\ y =/= (/) /\ E.z e. om y ~~ z) <-> (y (_ {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} /\ y =/= (/) /\ E.z e. om y ~~ z)))
13		eleq2 1535	. . . . . . . . 9 |- (x = {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} -> (|^|y e. x <-> |^|y e. {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)}))
14	12, 13	imbi12d 626	. . . . . . . 8 |- (x = {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} -> (((y (_ x /\ y =/= (/) /\ E.z e. om y ~~ z) -> |^|y e. x) <-> ((y (_ {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} /\ y =/= (/) /\ E.z e. om y ~~ z) -> |^|y e. {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)})))
15	14	albidv 1278	. . . . . . 7 |- (x = {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} -> (A.y((y (_ x /\ y =/= (/) /\ E.z e. om y ~~ z) -> |^|y e. x) <-> A.y((y (_ {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} /\ y =/= (/) /\ E.z e. om y ~~ z) -> |^|y e. {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)})))
16	10, 15	anbi12d 628	. . . . . 6 |- (x = {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} -> ((A (_ x /\ A.y((y (_ x /\ y =/= (/) /\ E.z e. om y ~~ z) -> |^|y e. x)) <-> (A (_ {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} /\ A.y((y (_ {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} /\ y =/= (/) /\ E.z e. om y ~~ z) -> |^|y e. {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)}))))
17		ssmin 2552	. . . . . . . 8 |- A (_ |^|{w | (A (_ w /\ A.v((v (_ A /\ v =/= (/) /\ E.u e. om v ~~ u) -> |^|v e. w))}
18	1	abfii3OLD 4563	. . . . . . . . 9 |- |^|{w | (A (_ w /\ A.v((v (_ A /\ v =/= (/) /\ E.u e. om v ~~ u) -> |^|v e. w))} = |^|{w | A.v((v (_ A /\ v =/= (/) /\ E.u e. om v ~~ u) -> |^|v e. w)}
19	1	abfii2OLD 4562	. . . . . . . . 9 |- {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} = |^|{w | A.v((v (_ A /\ v =/= (/) /\ E.u e. om v ~~ u) -> |^|v e. w)}
20	18, 19	eqtr4 1498	. . . . . . . 8 |- |^|{w | (A (_ w /\ A.v((v (_ A /\ v =/= (/) /\ E.u e. om v ~~ u) -> |^|v e. w))} = {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)}
21	17, 20	sseqtr 2093	. . . . . . 7 |- A (_ {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)}
22		eeanv 1323	. . . . . . . . . . . 12 |- (E.tE.f((t (_ A /\ E.u e. om t ~~ u /\ y = |^|t) /\ (f (_ A /\ E.u e. om f ~~ u /\ z = |^|f)) <-> (E.t(t (_ A /\ E.u e. om t ~~ u /\ y = |^|t) /\ E.f(f (_ A /\ E.u e. om f ~~ u /\ z = |^|f)))
23		an6 902	. . . . . . . . . . . . . 14 |- (((t (_ A /\ E.u e. om t ~~ u /\ y = |^|t) /\ (f (_ A /\ E.u e. om f ~~ u /\ z = |^|f)) <-> ((t (_ A /\ f (_ A) /\ (E.u e. om t ~~ u /\ E.u e. om f ~~ u) /\ (y = |^|t /\ z = |^|f)))
24		visset 1813	. . . . . . . . . . . . . . . . 17 |- t e. V
25		visset 1813	. . . . . . . . . . . . . . . . 17 |- f e. V
26	24, 25	unex 2872	. . . . . . . . . . . . . . . 16 |- (t u. f) e. V
27		sseq1 2082	. . . . . . . . . . . . . . . . 17 |- (v = (t u. f) -> (v (_ A <-> (t u. f) (_ A))
28		breq1 2622	. . . . . . . . . . . . . . . . . 18 |- (v = (t u. f) -> (v ~~ u <-> (t u. f) ~~ u))
29	28	rexbidv 1664	. . . . . . . . . . . . . . . . 17 |- (v = (t u. f) -> (E.u e. om v ~~ u <-> E.u e. om (t u. f) ~~ u))
30		inteq 2536	. . . . . . . . . . . . . . . . . 18 |- (v = (t u. f) -> |^|v = |^|(t u. f))
31	30	eqeq2d 1486	. . . . . . . . . . . . . . . . 17 |- (v = (t u. f) -> ((y i^i z) = |^|v <-> (y i^i z) = |^|(t u. f)))
32	27, 29, 31	3anbi123d 893	. . . . . . . . . . . . . . . 16 |- (v = (t u. f) -> ((v (_ A /\ E.u e. om v ~~ u /\ (y i^i z) = |^|v) <-> ((t u. f) (_ A /\ E.u e. om (t u. f) ~~ u /\ (y i^i z) = |^|(t u. f))))
33	26, 32	cla4ev 1869	. . . . . . . . . . . . . . 15 |- (((t u. f) (_ A /\ E.u e. om (t u. f) ~~ u /\ (y i^i z) = |^|(t u. f)) -> E.v(v (_ A /\ E.u e. om v ~~ u /\ (y i^i z) = |^|v))
34		unss 2204	. . . . . . . . . . . . . . . 16 |- ((t (_ A /\ f (_ A) <-> (t u. f) (_ A)
35	34	biimp 151	. . . . . . . . . . . . . . 15 |- ((t (_ A /\ f (_ A) -> (t u. f) (_ A)
36		unfiOLD 4552	. . . . . . . . . . . . . . 15 |- ((E.u e. om t ~~ u /\ E.u e. om f ~~ u) -> E.u e. om (t u. f) ~~ u)
37		ineq12 2212	. . . . . . . . . . . . . . . 16 |- ((y = |^|t /\ z = |^|f) -> (y i^i z) = (|^|t i^i |^|f))
38		intun 2562	. . . . . . . . . . . . . . . 16 |- |^|(t u. f) = (|^|t i^i |^|f)
39	37, 38	syl6eqr 1525	. . . . . . . . . . . . . . 15 |- ((y = |^|t /\ z = |^|f) -> (y i^i z) = |^|(t u. f))
40	33, 35, 36, 39	syl3an 868	. . . . . . . . . . . . . 14 |- (((t (_ A /\ f (_ A) /\ (E.u e. om t ~~ u /\ E.u e. om f ~~ u) /\ (y = |^|t /\ z = |^|f)) -> E.v(v (_ A /\ E.u e. om v ~~ u /\ (y i^i z) = |^|v))
41	23, 40	sylbi 199	. . . . . . . . . . . . 13 |- (((t (_ A /\ E.u e. om t ~~ u /\ y = |^|t) /\ (f (_ A /\ E.u e. om f ~~ u /\ z = |^|f)) -> E.v(v (_ A /\ E.u e. om v ~~ u /\ (y i^i z) = |^|v))
42	41	19.23aivv 1296	. . . . . . . . . . . 12 |- (E.tE.f((t (_ A /\ E.u e. om t ~~ u /\ y = |^|t) /\ (f (_ A /\ E.u e. om f ~~ u /\ z = |^|f)) -> E.v(v (_ A /\ E.u e. om v ~~ u /\ (y i^i z) = |^|v))
43	22, 42	sylbir 201	. . . . . . . . . . 11 |- (