Theorem abfii4 4538

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
abfii2.1	|- A e. V

Assertion

Ref	Expression
abfii4	|- |^|{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 abfii4

Step	Hyp	Ref	Expression
1		abfii2.1	. . . . . . 7 |- A e. V
2		df-sn 2402	. . . . . . . 8 |- {|^|v} = {w | w = |^|v}
3		snex 2740	. . . . . . . 8 |- {|^|v} e. V
4	2, 3	eqeltrr 1537	. . . . . . 7 |- {w | w = |^|v} e. V
5	1, 4	abexssex 3857	. . . . . 6 |- {w | E.v(v (_ A /\ w = |^|v)} e. V
6		3simpb 784	. . . . . . . 8 |- ((v (_ A /\ E.u e. om v ~~ u /\ w = |^|v) -> (v (_ A /\ w = |^|v))
7	6	19.22i 1036	. . . . . . 7 |- (E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v) -> E.v(v (_ A /\ w = |^|v))
8	7	ss2abi 2110	. . . . . 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 2710	. . . . 5 |- {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)} e. V
10		sseq2 2073	. . . . . . 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 2073	. . . . . . . . . 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 894	. . . . . . . . 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 1527	. . . . . . . . 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 624	. . . . . . . 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 1273	. . . . . . 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 626	. . . . . 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 2542	. . . . . . . 8 |- A (_ |^|{w | (A (_ w /\ A.v((v (_ A /\ v =/= (/) /\ E.u e. om v ~~ u) -> |^|v e. w))}
18	1	abfii3 4537	. . . . . . . . 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	abfii2 4536	. . . . . . . . 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 1490	. . . . . . . 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 2083	. . . . . . 7 |- A (_ {w | E.v(v (_ A /\ E.u e. om v ~~ u /\ w = |^|v)}
22		eeanv 1318	. . . . . . . . . . . 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 899	. . . . . . . . . . . . . 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 1804	. . . . . . . . . . . . . . . . 17 |- t e. V
25		visset 1804	. . . . . . . . . . . . . . . . 17 |- f e. V
26	24, 25	unex 2863	. . . . . . . . . . . . . . . 16 |- (t u. f) e. V
27		sseq1 2072	. . . . . . . . . . . . . . . . 17 |- (v = (t u. f) -> (v (_ A <-> (t u. f) (_ A))
28		breq1 2612	. . . . . . . . . . . . . . . . . 18 |- (v = (t u. f) -> (v ~~ u <-> (t u. f) ~~ u))
29	28	rexbidv 1656	. . . . . . . . . . . . . . . . 17 |- (v = (t u. f) -> (E.u e. om v ~~ u <-> E.u e. om (t u. f) ~~ u))
30		inteq 2526	. . . . . . . . . . . . . . . . . 18 |- (v = (t u. f) -> |^|v = |^|(t u. f))
31	30	eqeq2d 1478	. . . . . . . . . . . . . . . . 17 |- (v = (t u. f) -> ((y i^i z) = |^|v <-> (y i^i z) = |^|(t u. f)))
32	27, 29, 31	3anbi123d 890	. . . . . . . . . . . . . . . 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 1860	. . . . . . . . . . . . . . 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 2194	. . . . . . . . . . . . . . . 16 |- ((t (_ A /\ f (_ A) <-> (t u. f) (_ A)
35	34	biimp 151	. . . . . . . . . . . . . . 15 |- ((t (_ A /\ f (_ A) -> (t u. f) (_ A)
36		unfi 4528	. . . . . . . . . . . . . . 15 |- ((E.u e. om t ~~ u /\ E.u e. om f ~~ u) -> E.u e. om (t u. f) ~~ u)
37		ineq12 2202	. . . . . . . . . . . . . . . 16 |- ((y = |^|t /\ z = |^|f) -> (y i^i z) = (|^|t i^i |^|f))
38		intun 2552	. . . . . . . . . . . . . . . 16 |- |^|(t u. f) = (|^|t i^i |^|f)
39	37, 38	syl6eqr 1517	. . . . . . . . . . . . . . 15 |- ((y = |^|t /\ z = |^|f) -> (y i^i z) = |^|(t u. f))
40	33, 35, 36, 39	syl3an 866	. . . . . . . . . . . . . 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 1291	. . . . . . . . . . . 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 |- ((E.