Theorem ficli 10404

Description: The class of finite intersections of a class L are closed under intersection.

Hypothesis

Ref	Expression
ficli.1	|- F = {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)}

Assertion

Ref	Expression
ficli	|- ((A e. F /\ B e. F) -> (A i^i B) e. F)

Distinct variable groups:   y,A,x   y,B,x   y,L,x   y,z,x

Proof of Theorem ficli

Step	Hyp	Ref	Expression
1		spfi 10382	. . . . . . 7 |- (A e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)} -> (A e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)} <-> E.y(y (_ L /\ E.z e. om y ~~ z /\ A = |^|y)))
2	1	biimpd 153	. . . . . 6 |- (A e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)} -> (A e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)} -> E.y(y (_ L /\ E.z e. om y ~~ z /\ A = |^|y)))
3		spfi 10382	. . . . . . 7 |- (B e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)} -> (B e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)} <-> E.y(y (_ L /\ E.z e. om y ~~ z /\ B = |^|y)))
4	3	biimpd 153	. . . . . 6 |- (B e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)} -> (B e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)} -> E.y(y (_ L /\ E.z e. om y ~~ z /\ B = |^|y)))
5	2, 4	im2anan9 562	. . . . 5 |- ((A e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)} /\ B e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)}) -> ((A e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)} /\ B e. {x | E.y(y (_ L /\ E.z e. om y ~~ z /\ x = |^|y)}) -> (E.y(y (_ L /\ E.z e. om y ~~ z /\ A = |^|y) /\ E.y(y (_ L /\ E.z e. om y ~~ z /\ B = |^|y))))
6		an6 900	. . . . . . . . . . . . . 14 |- (((b (_ L /\ E.z e. om b ~~ z /\ B = |^|b) /\ (a (_ L /\ E.z e. om a ~~ z /\ A = |^|a)) <-> ((b (_ L /\ a (_ L) /\ (E.z e. om b ~~ z /\ E.z e. om a ~~ z) /\ (B = |^|b /\ A = |^|a)))
7		unss 2200	. . . . . . . . . . . . . . . . . . 19 |- ((a (_ L /\ b (_ L) <-> (a u. b) (_ L)
8	7	biimp 151	. . . . . . . . . . . . . . . . . 18 |- ((a (_ L /\ b (_ L) -> (a u. b) (_ L)
9	8	ancoms 436	. . . . . . . . . . . . . . . . 17 |- ((b (_ L /\ a (_ L) -> (a u. b) (_ L)
10		visset 1809	. . . . . . . . . . . . . . . . . . 19 |- a e. V
11		visset 1809	. . . . . . . . . . . . . . . . . . 19 |- b e. V
12	10, 11	unex 2867	. . . . . . . . . . . . . . . . . 18 |- (a u. b) e. V
13	12	elpw 2400	. . . . . . . . . . . . . . . . 17 |- ((a u. b) e. P~L <-> (a u. b) (_ L)
14	9, 13	sylibr 200	. . . . . . . . . . . . . . . 16 |- ((b (_ L /\ a (_ L) -> (a u. b) e. P~L)
15		unfi 4534	. . . . . . . . . . . . . . . . . 18 |- ((E.z e. om a ~~ z /\ E.z e. om b ~~ z) -> E.z e. om (a u. b) ~~ z)
16	15	ancoms 436	. . . . . . . . . . . . . . . . 17 |- ((E.z e. om b ~~ z /\ E.z e. om a ~~ z) -> E.z e. om (a u. b) ~~ z)
17		ineq12 2208	. . . . . . . . . . . . . . . . . . 19 |- ((A = |^|a /\ B = |^|b) -> (A i^i B) = (|^|a i^i |^|b))
18		intun 2557	. . . . . . . . . . . . . . . . . . 19 |- |^|(a u. b) = (|^|a i^i |^|b)
19	17, 18	syl6eqr 1522	. . . . . . . . . . . . . . . . . 18 |- ((A = |^|a /\ B = |^|b) -> (A i^i B) = |^|(a u. b))
20	19	ancoms 436	. . . . . . . . . . . . . . . . 17 |- ((B = |^|b /\ A = |^|a) -> (A i^i B) = |^|(a u. b))
21	16, 20	anim12i 333	. . . . . . . . . . . . . . . 16 |- (((E.z e. om b ~~ z /\ E.z e. om a ~~ z) /\ (B = |^|b /\ A = |^|a)) -> (E.z e. om (a u. b) ~~ z /\ (A i^i B) = |^|(a u. b)))
22	14, 21	anim12i 333	. . . . . . . . . . . . . . 15 |- (((b (_ L /\ a (_ L) /\ ((E.z e. om b ~~ z /\ E.z e. om a ~~ z) /\ (B = |^|b /\ A = |^|a))) -> ((a u. b) e. P~L /\ (E.z e. om (a u. b) ~~ z /\ (A i^i B) = |^|(a u. b))))
23	22	3impb 828	. . . . . . . . . . . . . 14 |- (((b (_ L /\ a (_ L) /\ (E.z e. om b ~~ z /\ E.z e. om a ~~ z) /\ (B = |^|b /\ A = |^|a)) -> ((a u. b) e. P~L /\ (E.z e. om (a u. b) ~~ z /\ (A i^i B) = |^|(a u. b))))
24	6, 23	sylbi 199	. . . . . . . . . . . . 13 |- (((b (_ L /\ E.z e. om b ~~ z /\ B = |^|b) /\ (a (_ L /\ E.z e. om a ~~ z /\ A = |^|a)) -> ((a u. b) e. P~L /\ (E.z e. om (a u. b) ~~ z /\ (A i^i B) = |^|(a u. b))))
25		breq1 2617	. . . . . . . . . . . . . . . 16 |- (y = (a u. b) -> (y ~~ z <-> (a u. b) ~~ z))
26	25	rexbidv 1661	. . . . . . . . . . . . . . 15 |- (y = (a u. b) -> (E.z e. om y ~~ z <-> E.z e. om (a u. b) ~~ z))
27		inteq 2531	. . . . . . . . . . . . . . . 16 |- (y = (a u. b) -> |^|y = |^|(a u. b))
28	27	eqeq2d 1483	. . . . . . . . . . . . . . 15 |- (y = (a u. b) -> ((A i^i B) = |^|y <-> (A i^i B) = |^|(a u. b)))
29	26, 28	anbi12d 627	. . . . . . . . . . . . . 14 |- (y = (a u. b) -> ((E.z e. om y ~~ z /\ (A i^i B) = |^|y) <-> (E.z e. om (a u. b) ~~ z /\ (A i^i B) = |^|(a u. b))))
30	29	rcla4ev 1873	. . . . . . . . . . . . 13 |- (((a u. b) e. P~L /\ (E.z e. om (a u. b) ~~ z /\ (A i^i B) = |^|(a u. b))) -> E.y e. P~ L(E.z e. om y ~~ z /\ (A i^i B) = |^|y))
31	24, 30	syl 10	. . . . . . . . . . . 12 |- (((b (_ L /\ E.z e. om b ~~ z /\ B = |^|b) /\ (a (_ L /\ E.z e. om a ~~ z /\ A = |^|a)) -> E.y e. P~ L(E.z e. om y ~~ z /\ (A i^i B) = |^|y))
32		visset 1809	. . . . . . . . . . . . . . . . . 18 |- y e. V
33	32	elpw 2400	. . . . . . . . . . . . . . . . 17 |- (y e. P~L <-> y (_ L)
34	33	bicomi 172	. . . . . . . . . . . . . . . 16 |- (y (_ L <-> y e. P~L)
35	34	3anbi1i 823	. . . . . . . . . . . . . . 15 |- ((y (_ L /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y) <-> (y e. P~L /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y))
36		3anass 778	. . . . . . . . . . . . . . 15 |- ((y e. P~L /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y) <-> (y e. P~L /\ (E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
37	35, 36	bitr 173	. . . . . . . . . . . . . 14 |- ((y (_ L /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y) <-> (y e. P~L /\ (E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
38	37	exbii 1049	. . . . . . . . . . . . 13 |- (E.y(y (_ L /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y) <-> E.y(y e. P~L /\ (E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
39		df-rex 1647	. . . . . . . . . . . . 13 |- (E.y e. P~ L(E.z e. om y ~~ z /\ (A i^i B) = |^|y) <-> E.y(y e. P~L /\ (E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
40	38, 39	bitr4 176	. . . . . . . . . . . 12 |- (E.y(y (_ L /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y) <-> E.y e. P~ L(E.z e. om y ~~ z /\ (A i^i B) = |^|y))
41	31, 40	sylibr 200	. . . . . . . . . . 11 |- (((b (_ L /\ E.z e. om b ~~ z /\ B = |^|b) /\ (a (_ L /\ E.z e. om a ~~ z /\ A = |^|a)) -> E.y(y (_ L /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y))
42	41	ex 373	. . . . . . . . . 10 |- ((b (_ L /\ E.z e. om b ~~ z /\ B = |^|b) -> ((a (_ L /\ E.z e. om a ~~ z /\ A = |^|a) -> E.y(y (_ L /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
43	42	19.23aiv 1293	. . . . . . . . 9 |- (E.b(b (_ L /\ E.z e. om b ~~ z /\ B = |^|b) -> ((a (_ L /\ E.z e. om a ~~ z /\ A = |^|a) -> E.y(y (_ L /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
44	43	com12 11