Theorem ficli 10472

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

Hypothesis

Ref	Expression
ficliNEW.1	|- F = {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)}

Assertion

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

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

Proof of Theorem ficli

Step	Hyp	Ref	Expression
1		spfi 10445	. . . . . . 7 |- (A e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)} -> (A e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)} <-> E.y(y (_ L /\ y e. Fin /\ A = |^|y)))
2	1	biimpd 153	. . . . . 6 |- (A e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)} -> (A e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)} -> E.y(y (_ L /\ y e. Fin /\ A = |^|y)))
3		spfi 10445	. . . . . . 7 |- (B e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)} -> (B e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)} <-> E.y(y (_ L /\ y e. Fin /\ B = |^|y)))
4	3	biimpd 153	. . . . . 6 |- (B e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)} -> (B e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)} -> E.y(y (_ L /\ y e. Fin /\ B = |^|y)))
5	2, 4	im2anan9 563	. . . . 5 |- ((A e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)} /\ B e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)}) -> ((A e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)} /\ B e. {x | E.y(y (_ L /\ y e. Fin /\ x = |^|y)}) -> (E.y(y (_ L /\ y e. Fin /\ A = |^|y) /\ E.y(y (_ L /\ y e. Fin /\ B = |^|y))))
6		an6 902	. . . . . . . . . . . . . 14 |- (((b (_ L /\ b e. Fin /\ B = |^|b) /\ (a (_ L /\ a e. Fin /\ A = |^|a)) <-> ((b (_ L /\ a (_ L) /\ (b e. Fin /\ a e. Fin) /\ (B = |^|b /\ A = |^|a)))
7		unss 2204	. . . . . . . . . . . . . . . . . . 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 1813	. . . . . . . . . . . . . . . . . . 19 |- a e. V
11		visset 1813	. . . . . . . . . . . . . . . . . . 19 |- b e. V
12	10, 11	unex 2872	. . . . . . . . . . . . . . . . . 18 |- (a u. b) e. V
13	12	elpw 2404	. . . . . . . . . . . . . . . . 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 4551	. . . . . . . . . . . . . . . . . 18 |- ((a e. Fin /\ b e. Fin) -> (a u. b) e. Fin)
16	15	ancoms 436	. . . . . . . . . . . . . . . . 17 |- ((b e. Fin /\ a e. Fin) -> (a u. b) e. Fin)
17		ineq12 2212	. . . . . . . . . . . . . . . . . . 19 |- ((A = |^|a /\ B = |^|b) -> (A i^i B) = (|^|a i^i |^|b))
18		intun 2562	. . . . . . . . . . . . . . . . . . 19 |- |^|(a u. b) = (|^|a i^i |^|b)
19	17, 18	syl6eqr 1525	. . . . . . . . . . . . . . . . . 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 |- (((b e. Fin /\ a e. Fin) /\ (B = |^|b /\ A = |^|a)) -> ((a u. b) e. Fin /\ (A i^i B) = |^|(a u. b)))
22	14, 21	anim12i 333	. . . . . . . . . . . . . . 15 |- (((b (_ L /\ a (_ L) /\ ((b e. Fin /\ a e. Fin) /\ (B = |^|b /\ A = |^|a))) -> ((a u. b) e. P~L /\ ((a u. b) e. Fin /\ (A i^i B) = |^|(a u. b))))
23	22	3impb 829	. . . . . . . . . . . . . 14 |- (((b (_ L /\ a (_ L) /\ (b e. Fin /\ a e. Fin) /\ (B = |^|b /\ A = |^|a)) -> ((a u. b) e. P~L /\ ((a u. b) e. Fin /\ (A i^i B) = |^|(a u. b))))
24	6, 23	sylbi 199	. . . . . . . . . . . . 13 |- (((b (_ L /\ b e. Fin /\ B = |^|b) /\ (a (_ L /\ a e. Fin /\ A = |^|a)) -> ((a u. b) e. P~L /\ ((a u. b) e. Fin /\ (A i^i B) = |^|(a u. b))))
25		eleq1 1534	. . . . . . . . . . . . . . 15 |- (y = (a u. b) -> (y e. Fin <-> (a u. b) e. Fin))
26		inteq 2536	. . . . . . . . . . . . . . . 16 |- (y = (a u. b) -> |^|y = |^|(a u. b))
27	26	eqeq2d 1486	. . . . . . . . . . . . . . 15 |- (y = (a u. b) -> ((A i^i B) = |^|y <-> (A i^i B) = |^|(a u. b)))
28	25, 27	anbi12d 628	. . . . . . . . . . . . . 14 |- (y = (a u. b) -> ((y e. Fin /\ (A i^i B) = |^|y) <-> ((a u. b) e. Fin /\ (A i^i B) = |^|(a u. b))))
29	28	rcla4ev 1877	. . . . . . . . . . . . 13 |- (((a u. b) e. P~L /\ ((a u. b) e. Fin /\ (A i^i B) = |^|(a u. b))) -> E.y e. P~ L(y e. Fin /\ (A i^i B) = |^|y))
30	24, 29	syl 10	. . . . . . . . . . . 12 |- (((b (_ L /\ b e. Fin /\ B = |^|b) /\ (a (_ L /\ a e. Fin /\ A = |^|a)) -> E.y e. P~ L(y e. Fin /\ (A i^i B) = |^|y))
31		visset 1813	. . . . . . . . . . . . . . . . . 18 |- y e. V
32	31	elpw 2404	. . . . . . . . . . . . . . . . 17 |- (y e. P~L <-> y (_ L)
33	32	bicomi 172	. . . . . . . . . . . . . . . 16 |- (y (_ L <-> y e. P~L)
34	33	3anbi1i 824	. . . . . . . . . . . . . . 15 |- ((y (_ L /\ y e. Fin /\ (A i^i B) = |^|y) <-> (y e. P~L /\ y e. Fin /\ (A i^i B) = |^|y))
35		3anass 779	. . . . . . . . . . . . . . 15 |- ((y e. P~L /\ y e. Fin /\ (A i^i B) = |^|y) <-> (y e. P~L /\ (y e. Fin /\ (A i^i B) = |^|y)))
36	34, 35	bitr 173	. . . . . . . . . . . . . 14 |- ((y (_ L /\ y e. Fin /\ (A i^i B) = |^|y) <-> (y e. P~L /\ (y e. Fin /\ (A i^i B) = |^|y)))
37	36	exbii 1051	. . . . . . . . . . . . 13 |- (E.y(y (_ L /\ y e. Fin /\ (A i^i B) = |^|y) <-> E.y(y e. P~L /\ (y e. Fin /\ (A i^i B) = |^|y)))
38		df-rex 1650	. . . . . . . . . . . . 13 |- (E.y e. P~ L(y e. Fin /\ (A i^i B) = |^|y) <-> E.y(y e. P~L /\ (y e. Fin /\ (A i^i B) = |^|y)))
39	37, 38	bitr4 176	. . . . . . . . . . . 12 |- (E.y(y (_ L /\ y e. Fin /\ (A i^i B) = |^|y) <-> E.y e. P~ L(y e. Fin /\ (A i^i B) = |^|y))
40	30, 39	sylibr 200	. . . . . . . . . . 11 |- (((b (_ L /\ b e. Fin /\ B = |^|b) /\ (a (_ L /\ a e. Fin /\ A = |^|a)) -> E.y(y (_ L /\ y e. Fin /\ (A i^i B) = |^|y))
41	40	ex 373	. . . . . . . . . 10 |- ((b (_ L /\ b e. Fin /\ B = |^|b) -> ((a (_ L /\ a e. Fin /\ A = |^|a) -> E.y(y (_ L /\ y e. Fin /\ (A i^i B) = |^|y)))
42	41	19.23aiv 1295	. . . . . . . . 9 |- (E.b(b (_ L /\ b e. Fin /\ B = |^|b) -> ((a (_ L /\ a e. Fin /\ A = |^|a) -> E.y(y (_ L /\ y e. Fin /\ (A i^i B) = |^|y)))
43	42	com12 11	. . . . . . . 8 |- ((a (_ L /\ a e. Fin /\ A = |^|a) -> (E.b(b (_ L /\ b e. Fin /\ B = |^|b) -> E.y(y (_ L /\ y e. Fin /\ (A i^i B) = |^|y)))
44	43	19.23aiv 1295	. . . . . . 7 |- (E.a(a (_ L /\ a e. Fin /\ A = |^|a) -> (E.b(b (_ L /\ b e. Fin /\ B = |^|b) -> E.y(y (_ L /\ y e. Fin /\ (A i^i B) = |^|y)))
45	44	imp 350	. . . . . 6 |- ((E.a(a (_ L /\ a e. Fin /\ A = |^|a) /\ E.b(b (_ L /\ b e. Fin /\ B = |^|b)) -> E.y(y (_ L /\ y e. Fin /\ (A i^i B) = |^|y))
46		sseq1 2082	. . . . . . . 8 |- (y = a -> (y (_ L <-> a (_ L))
47		eleq1 1534	. . . . . . . 8 |- (y = a -> (y e. Fin <-> a e. Fin))
48		inteq 2536	. . . . . . . . 9 |- (y = a -> |^|y = |^|a)
49	48	eqeq2d 1486	. . . . . . . 8 |- (y = a -> (A = |^|y <-> A = |^|a))
50	46, 47, 49	3anbi123d 893	. . . . . . 7 |- (y = a -> ((y (_ L /\ y e. Fin /\ A = |^|y) <-> (a (_ L /\ a e. Fin /\ A = |^|a)))
51	50	cbvexv 1315	. . . . . 6 |- (E.y