Theorem fiiu 10350

Description: If A is the intersection of a finite set of elements of B then A (_ U.B.

Assertion

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

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

Proof of Theorem fiiu

Step	Hyp	Ref	Expression
1		nvel 2704	. . . 4 |- -. V e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)}
2		eleq1 1526	. . . . 5 |- (A = V -> (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} <-> V e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)}))
3	2	biimpcd 155	. . . 4 |- (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} -> (A = V -> V e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)}))
4	1, 3	mtoi 107	. . 3 |- (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} -> -. A = V)
5		spfi 10346	. . . 4 |- (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} -> (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} <-> E.y(y (_ B /\ E.z e. om y ~~ z /\ A = |^|y)))
6		eqeq1 1473	. . . . . . . . . . . 12 |- (A = |^|y -> (A = V <-> |^|y = V))
7	6	negbid 609	. . . . . . . . . . 11 |- (A = |^|y -> (-. A = V <-> -. |^|y = V))
8	7	biimpd 153	. . . . . . . . . 10 |- (A = |^|y -> (-. A = V -> -. |^|y = V))
9		int0 2537	. . . . . . . . . . 11 |- |^|(/) = V
10		eqeq2 1476	. . . . . . . . . . . . . 14 |- (|^|(/) = V -> (|^|y = |^|(/) <-> |^|y = V))
11	10	bicomd 519	. . . . . . . . . . . . 13 |- (|^|(/) = V -> (|^|y = V <-> |^|y = |^|(/)))
12	11	negbid 609	. . . . . . . . . . . 12 |- (|^|(/) = V -> (-. |^|y = V <-> -. |^|y = |^|(/)))
13		inteq 2526	. . . . . . . . . . . . . 14 |- (y = (/) -> |^|y = |^|(/))
14	13	con3i 98	. . . . . . . . . . . . 13 |- (-. |^|y = |^|(/) -> -. y = (/))
15		sseq1 2072	. . . . . . . . . . . . . . . . . 18 |- (|^|y = A -> (|^|y (_ U.B <-> A (_ U.B))
16	15	biimpd 153	. . . . . . . . . . . . . . . . 17 |- (|^|y = A -> (|^|y (_ U.B -> A (_ U.B))
17	16	eqcoms 1470	. . . . . . . . . . . . . . . 16 |- (A = |^|y -> (|^|y (_ U.B -> A (_ U.B))
18		intssuni2 2546	. . . . . . . . . . . . . . . . . . 19 |- ((y (_ B /\ y =/= (/)) -> |^|y (_ U.B)
19		df-ne 1579	. . . . . . . . . . . . . . . . . . 19 |- (y =/= (/) <-> -. y = (/))
20	18, 19	sylan2br 453	. . . . . . . . . . . . . . . . . 18 |- ((y (_ B /\ -. y = (/)) -> |^|y (_ U.B)
21	20	ancoms 436	. . . . . . . . . . . . . . . . 17 |- ((-. y = (/) /\ y (_ B) -> |^|y (_ U.B)
22	21	3adant2 796	. . . . . . . . . . . . . . . 16 |- ((-. y = (/) /\ E.z e. om y ~~ z /\ y (_ B) -> |^|y (_ U.B)
23	17, 22	syl5com 52	. . . . . . . . . . . . . . 15 |- ((-. y = (/) /\ E.z e. om y ~~ z /\ y (_ B) -> (A = |^|y -> A (_ U.B))
24	23	3exp 830	. . . . . . . . . . . . . 14 |- (-. y = (/) -> (E.z e. om y ~~ z -> (y (_ B -> (A = |^|y -> A (_ U.B))))
25	24	com24 37	. . . . . . . . . . . . 13 |- (-. y = (/) -> (A = |^|y -> (y (_ B -> (E.z e. om y ~~ z -> A (_ U.B))))
26	14, 25	syl 10	. . . . . . . . . . . 12 |- (-. |^|y = |^|(/) -> (A = |^|y -> (y (_ B -> (E.z e. om y ~~ z -> A (_ U.B))))
27	12, 26	syl6bi 214	. . . . . . . . . . 11 |- (|^|(/) = V -> (-. |^|y = V -> (A = |^|y -> (y (_ B -> (E.z e. om y ~~ z -> A (_ U.B)))))
28	9, 27	ax-mp 7	. . . . . . . . . 10 |- (-. |^|y = V -> (A = |^|y -> (y (_ B -> (E.z e. om y ~~ z -> A (_ U.B))))
29	8, 28	syl6com 53	. . . . . . . . 9 |- (-. A = V -> (A = |^|y -> (A = |^|y -> (y (_ B -> (E.z e. om y ~~ z -> A (_ U.B)))))
30	29	com13 33	. . . . . . . 8 |- (A = |^|y -> (A = |^|y -> (-. A = V -> (y (_ B -> (E.z e. om y ~~ z -> A (_ U.B)))))
31	30	pm2.43i 64	. . . . . . 7 |- (A = |^|y -> (-. A = V -> (y (_ B -> (E.z e. om y ~~ z -> A (_ U.B))))
32	31	com4t 40	. . . . . 6 |- (y (_ B -> (E.z e. om y ~~ z -> (A = |^|y -> (-. A = V -> A (_ U.B))))
33	32	3imp 825	. . . . 5 |- ((y (_ B /\ E.z e. om y ~~ z /\ A = |^|y) -> (-. A = V -> A (_ U.B))
34	33	19.23aiv 1290	. . . 4 |- (E.y(y (_ B /\ E.z e. om y ~~ z /\ A = |^|y) -> (-. A = V -> A (_ U.B))
35	5, 34	syl6bi 214	. . 3 |- (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} -> (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} -> (-. A = V -> A (_ U.B)))
36	4, 35	mpid 47	. 2 |- (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} -> (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} -> A (_ U.B))
37	36	pm2.43i 64	1 |- (A e. {x | E.y(y (_ B /\ E.z e. om y ~~ z /\ x = |^|y)} -> A (_ U.B)

Syntax hints:  -. wn 2   -> wi 3   /\ w3a 773   = wceq 953   e. wcel 955  E.wex 977  {cab 1456   =/= wne 1577  E.wrex 1638  Vcvv 1802   (_ wss 2037  (/)c0 2270  U.cuni 2493  |^|cint 2523   class class class wbr 2609  omcom 3121   ~~ cen 4348

This theorem is referenced by:  fgsb 10444

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-in 2041  df-ss 2043  df-nul 2271  df-uni 2494  df-int 2524

Copyright terms: Public domain