Theorem infi1 10383

Description: The intersection of two finite intersections is a finite intersection.

Assertion

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

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

Proof of Theorem infi1

Step	Hyp	Ref	Expression
1		inex1g 2713	. . . 4 |- (A e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)} -> (A i^i B) e. V)
2	1	adantr 389	. . 3 |- ((A e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)} /\ B e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)}) -> (A i^i B) e. V)
3		spfi 10382	. . . . . . 7 |- (A e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)} -> (A e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)} <-> E.y(y (_ C /\ E.z e. om y ~~ z /\ A = |^|y)))
4		spfi 10382	. . . . . . . . . 10 |- (B e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)} -> (B e. {x | E.y(y (_ C /\ E.z e. om y ~~ z /\ x = |^|y)} <-> E.y(y (_ C /\ E.z e. om y ~~ z /\ B = |^|y)))
5		sseq1 2078	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (a u. b) -> (y (_ C <-> (a u. b) (_ C))
6		breq1 2617	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = (a u. b) -> (y ~~ z <-> (a u. b) ~~ z))
7	6	rexbidv 1661	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (a u. b) -> (E.z e. om y ~~ z <-> E.z e. om (a u. b) ~~ z))
8		inteq 2531	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = (a u. b) -> |^|y = |^|(a u. b))
9	8	eqeq2d 1483	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = (a u. b) -> ((A i^i B) = |^|y <-> (A i^i B) = |^|(a u. b)))
10	5, 7, 9	3anbi123d 891	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (a u. b) -> ((y (_ C /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y) <-> ((a u. b) (_ C /\ E.z e. om (a u. b) ~~ z /\ (A i^i B) = |^|(a u. b))))
11	10	cla4egv 1859	. . . . . . . . . . . . . . . . . . . 20 |- ((a u. b) e. V -> (((a u. b) (_ C /\ E.z e. om (a u. b) ~~ z /\ (A i^i B) = |^|(a u. b)) -> E.y(y (_ C /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
12		visset 1809	. . . . . . . . . . . . . . . . . . . . . 22 |- a e. V
13		visset 1809	. . . . . . . . . . . . . . . . . . . . . 22 |- b e. V
14	12, 13	unex 2867	. . . . . . . . . . . . . . . . . . . . 21 |- (a u. b) e. V
15	14	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (((a (_ C /\ E.z e. om a ~~ z /\ B = |^|a) /\ (b (_ C /\ E.z e. om b ~~ z /\ A = |^|b)) -> (a u. b) e. V)
16		an6 900	. . . . . . . . . . . . . . . . . . . . 21 |- (((a (_ C /\ E.z e. om a ~~ z /\ B = |^|a) /\ (b (_ C /\ E.z e. om b ~~ z /\ A = |^|b)) <-> ((a (_ C /\ b (_ C) /\ (E.z e. om a ~~ z /\ E.z e. om b ~~ z) /\ (B = |^|a /\ A = |^|b)))
17		unss 2200	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((a (_ C /\ b (_ C) <-> (a u. b) (_ C)
18	17	biimp 151	. . . . . . . . . . . . . . . . . . . . . 22 |- ((a (_ C /\ b (_ C) -> (a u. b) (_ C)
19		unfi 4534	. . . . . . . . . . . . . . . . . . . . . 22 |- ((E.z e. om a ~~ z /\ E.z e. om b ~~ z) -> E.z e. om (a u. b) ~~ z)
20		ineq2 2207	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (B = |^|a -> (A i^i B) = (A i^i |^|a))
21	20	adantr 389	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((B = |^|a /\ A = |^|b) -> (A i^i B) = (A i^i |^|a))
22		ineq1 2206	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A = |^|b -> (A i^i |^|a) = (|^|b i^i |^|a))
23	22	adantl 388	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((B = |^|a /\ A = |^|b) -> (A i^i |^|a) = (|^|b i^i |^|a))
24		incom 2204	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (|^|b i^i |^|a) = (|^|a i^i |^|b)
25		intun 2557	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- |^|(a u. b) = (|^|a i^i |^|b)
26	24, 25	eqtr4 1495	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (|^|b i^i |^|a) = |^|(a u. b)
27	26	a1i 8	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((B = |^|a /\ A = |^|b) -> (|^|b i^i |^|a) = |^|(a u. b))
28	21, 23, 27	3eqtrd 1508	. . . . . . . . . . . . . . . . . . . . . 22 |- ((B = |^|a /\ A = |^|b) -> (A i^i B) = |^|(a u. b))
29	18, 19, 28	3anim123i 820	. . . . . . . . . . . . . . . . . . . . 21 |- (((a (_ C /\ b (_ C) /\ (E.z e. om a ~~ z /\ E.z e. om b ~~ z) /\ (B = |^|a /\ A = |^|b)) -> ((a u. b) (_ C /\ E.z e. om (a u. b) ~~ z /\ (A i^i B) = |^|(a u. b)))
30	16, 29	sylbi 199	. . . . . . . . . . . . . . . . . . . 20 |- (((a (_ C /\ E.z e. om a ~~ z /\ B = |^|a) /\ (b (_ C /\ E.z e. om b ~~ z /\ A = |^|b)) -> ((a u. b) (_ C /\ E.z e. om (a u. b) ~~ z /\ (A i^i B) = |^|(a u. b)))
31	11, 15, 30	sylc 68	. . . . . . . . . . . . . . . . . . 19 |- (((a (_ C /\ E.z e. om a ~~ z /\ B = |^|a) /\ (b (_ C /\ E.z e. om b ~~ z /\ A = |^|b)) -> E.y(y (_ C /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y))
32	31	expcom 374	. . . . . . . . . . . . . . . . . 18 |- ((b (_ C /\ E.z e. om b ~~ z /\ A = |^|b) -> ((a (_ C /\ E.z e. om a ~~ z /\ B = |^|a) -> E.y(y (_ C /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
33	32	19.23aiv 1293	. . . . . . . . . . . . . . . . 17 |- (E.b(b (_ C /\ E.z e. om b ~~ z /\ A = |^|b) -> ((a (_ C /\ E.z e. om a ~~ z /\ B = |^|a) -> E.y(y (_ C /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
34	33	com12 11	. . . . . . . . . . . . . . . 16 |- ((a (_ C /\ E.z e. om a ~~ z /\ B = |^|a) -> (E.b(b (_ C /\ E.z e. om b ~~ z /\ A = |^|b) -> E.y(y (_ C /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
35	34	19.23aiv 1293	. . . . . . . . . . . . . . 15 |- (E.a(a (_ C /\ E.z e. om a ~~ z /\ B = |^|a) -> (E.b(b (_ C /\ E.z e. om b ~~ z /\ A = |^|b) -> E.y(y (_ C /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y)))
36	35	imp 350	. . . . . . . . . . . . . 14 |- ((E.a(a (_ C /\ E.z e. om a ~~ z /\ B = |^|a) /\ E.b(b (_ C /\ E.z e. om b ~~ z /\ A = |^|b)) -> E.y(y (_ C /\ E.z e. om y ~~ z /\ (A i^i B) = |^|y))
37		sseq1 2078	. . . . . . . . . . . . . . . 16 |- (y = a -> (y (_ C <-> a (_ C))
38		breq1 2617	. . . . . . . . . . . . . . . . 17 |- (y = a -> (y ~~ z <-> a ~~ z))
39	38	rexbidv 1661	. . . . . . . . . . . . . . . 16 |- (y = a -> (E.z e. om y ~~ z <-> E.z e. om a ~~ z))
40		inteq 2531	. . . . . . . . . . . . . . . . 17 |- (y = a -> |^|y = |^|a)
41	40	eqeq2d 1483	. . . . . . . . . . . . . . . 16 |- (y = a -> (B = |^|y <-> B = |^|a))
42	37, 39, 41	3anbi123d 891	. . . . . . . . . . . . . . 15 |- (y = a -> ((y (_ C /\ E.z e. om y ~~ z /\ B = |^|y) <-> (a (_ C /\ E.z e. om a ~~ z /\ B = |^|a)))
43	42	cbvexv 1313	. . . . . . . . . . . . . 14 |- (E.y(y (_ C /\ E.z e. om y ~~ z /\ B = |^|y) <-> E.a(a (_ C /\ E.z e. om a ~~ z /\ B = |^|a))
44		sseq1 2078	. . . . . . . . . . . . . . . 16 |- (y = b -> (y (_ C <-> b (_ C))
45		breq1 2617	. . . . . . . . . . . . . . . . 17 |- (y = b -> (y ~~ z <-> b ~~ z))
46	45	rexbidv 1661	. . . . . . . . . . . . . . . 16 |- (y = b -> (E.z e. om y ~~ z <-> E.z e. om b ~~ z))
47		inteq 2531	. . . . . . . . . . . . . . . . 17 |- (y = b -> |^|y = |^|b)
48	47	eqeq2d 1483	. . . . . . . . . . . . . . . 16 |- (y = b -> (A = |^|y <-> A = |^|b))
49	44, 46, 48	3anbi123d 891	. . . . . . . . . . . . . . 15 |- (y = b -> ((y (_ C /\ E.z e. om y ~~ z /\ A = |^|y) <-> (b (_ C /\ E.z e. om b ~~ z /\ A = |^|b)))
50	49	cbvexv 1313	. . . . . . . . . . . . . 14 |- (E.y(y (_ C /\ E.z e. om y ~~ z /\ A = |^|y) <-> E.b(b (_ C /\ E.z e. om b ~~ z /\ A = |^|b))
51	36, 43, 50	syl2anb 455	. . . . . . . . . . . . 13 |- ((E.y(y (_ C /\ E.z e. om y ~~ z /\ B = |^|y) /\ E.y