elfiun

Description: A finite intersection of elements taken from a union of collections. (Contributed by Jeff Hankins, 15-Nov-2009) (Proof shortened by Mario Carneiro, 26-Nov-2013)

		Ref	Expression
	Assertion	elfiun	\|- ( ( B e. D /\ C e. K ) -> ( A e. ( fi ` ( B u. C ) ) <-> ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	\|- ( A e. ( fi ` ( B u. C ) ) -> A e. _V )
2	1	adantl	\|- ( ( ( B e. D /\ C e. K ) /\ A e. ( fi ` ( B u. C ) ) ) -> A e. _V )
3		simpll	\|- ( ( ( B e. D /\ C e. K ) /\ A e. ( fi ` ( B u. C ) ) ) -> B e. D )
4		simplr	\|- ( ( ( B e. D /\ C e. K ) /\ A e. ( fi ` ( B u. C ) ) ) -> C e. K )
5	2 3 4	3jca	\|- ( ( ( B e. D /\ C e. K ) /\ A e. ( fi ` ( B u. C ) ) ) -> ( A e. _V /\ B e. D /\ C e. K ) )
6		elex	\|- ( A e. ( fi ` B ) -> A e. _V )
7	6	3anim1i	\|- ( ( A e. ( fi ` B ) /\ B e. D /\ C e. K ) -> ( A e. _V /\ B e. D /\ C e. K ) )
8	7	3expib	\|- ( A e. ( fi ` B ) -> ( ( B e. D /\ C e. K ) -> ( A e. _V /\ B e. D /\ C e. K ) ) )
9		elex	\|- ( A e. ( fi ` C ) -> A e. _V )
10	9	3anim1i	\|- ( ( A e. ( fi ` C ) /\ B e. D /\ C e. K ) -> ( A e. _V /\ B e. D /\ C e. K ) )
11	10	3expib	\|- ( A e. ( fi ` C ) -> ( ( B e. D /\ C e. K ) -> ( A e. _V /\ B e. D /\ C e. K ) ) )
12		vex	\|- x e. _V
13	12	inex1	\|- ( x i^i y ) e. _V
14		eleq1	\|- ( A = ( x i^i y ) -> ( A e. _V <-> ( x i^i y ) e. _V ) )
15	13 14	mpbiri	\|- ( A = ( x i^i y ) -> A e. _V )
16	15	a1i	\|- ( ( x e. ( fi ` B ) /\ y e. ( fi ` C ) ) -> ( A = ( x i^i y ) -> A e. _V ) )
17	16	rexlimivv	\|- ( E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) -> A e. _V )
18	17	3anim1i	\|- ( ( E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) /\ B e. D /\ C e. K ) -> ( A e. _V /\ B e. D /\ C e. K ) )
19	18	3expib	\|- ( E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) -> ( ( B e. D /\ C e. K ) -> ( A e. _V /\ B e. D /\ C e. K ) ) )
20	8 11 19	3jaoi	\|- ( ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) -> ( ( B e. D /\ C e. K ) -> ( A e. _V /\ B e. D /\ C e. K ) ) )
21	20	impcom	\|- ( ( ( B e. D /\ C e. K ) /\ ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) -> ( A e. _V /\ B e. D /\ C e. K ) )
22		simp1	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> A e. _V )
23		unexg	\|- ( ( B e. D /\ C e. K ) -> ( B u. C ) e. _V )
24	23	3adant1	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( B u. C ) e. _V )
25		elfi	\|- ( ( A e. _V /\ ( B u. C ) e. _V ) -> ( A e. ( fi ` ( B u. C ) ) <-> E. z e. ( ~P ( B u. C ) i^i Fin ) A = \|^\| z ) )
26	22 24 25	syl2anc	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( A e. ( fi ` ( B u. C ) ) <-> E. z e. ( ~P ( B u. C ) i^i Fin ) A = \|^\| z ) )
27		simpl1	\|- ( ( ( A e. _V /\ B e. D /\ C e. K ) /\ z e. ( ~P ( B u. C ) i^i Fin ) ) -> A e. _V )
28		eleq1	\|- ( A = \|^\| z -> ( A e. _V <-> \|^\| z e. _V ) )
29		intex	\|- ( z =/= (/) <-> \|^\| z e. _V )
30	28 29	bitr4di	\|- ( A = \|^\| z -> ( A e. _V <-> z =/= (/) ) )
31	27 30	syl5ibcom	\|- ( ( ( A e. _V /\ B e. D /\ C e. K ) /\ z e. ( ~P ( B u. C ) i^i Fin ) ) -> ( A = \|^\| z -> z =/= (/) ) )
32		simp22	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> B e. D )
33		inss2	\|- ( z i^i B ) C_ B
34	33	a1i	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( z i^i B ) C_ B )
35		simp1l	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( z i^i B ) =/= (/) )
36		simp3l	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z e. ( ~P ( B u. C ) i^i Fin ) )
37	36	elin2d	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z e. Fin )
38		inss1	\|- ( z i^i B ) C_ z
39		ssfi	\|- ( ( z e. Fin /\ ( z i^i B ) C_ z ) -> ( z i^i B ) e. Fin )
40	37 38 39	sylancl	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( z i^i B ) e. Fin )
41		elfir	\|- ( ( B e. D /\ ( ( z i^i B ) C_ B /\ ( z i^i B ) =/= (/) /\ ( z i^i B ) e. Fin ) ) -> \|^\| ( z i^i B ) e. ( fi ` B ) )
42	32 34 35 40 41	syl13anc	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> \|^\| ( z i^i B ) e. ( fi ` B ) )
43		simp23	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> C e. K )
44		inss2	\|- ( z i^i C ) C_ C
45	44	a1i	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( z i^i C ) C_ C )
46		simp1r	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( z i^i C ) =/= (/) )
47		inss1	\|- ( z i^i C ) C_ z
48		ssfi	\|- ( ( z e. Fin /\ ( z i^i C ) C_ z ) -> ( z i^i C ) e. Fin )
49	37 47 48	sylancl	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( z i^i C ) e. Fin )
50		elfir	\|- ( ( C e. K /\ ( ( z i^i C ) C_ C /\ ( z i^i C ) =/= (/) /\ ( z i^i C ) e. Fin ) ) -> \|^\| ( z i^i C ) e. ( fi ` C ) )
51	43 45 46 49 50	syl13anc	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> \|^\| ( z i^i C ) e. ( fi ` C ) )
52		elinel1	\|- ( z e. ( ~P ( B u. C ) i^i Fin ) -> z e. ~P ( B u. C ) )
53	52	elpwid	\|- ( z e. ( ~P ( B u. C ) i^i Fin ) -> z C_ ( B u. C ) )
54		dfss2	\|- ( z C_ ( B u. C ) <-> ( z i^i ( B u. C ) ) = z )
55	54	biimpi	\|- ( z C_ ( B u. C ) -> ( z i^i ( B u. C ) ) = z )
56		indi	\|- ( z i^i ( B u. C ) ) = ( ( z i^i B ) u. ( z i^i C ) )
57	55 56	eqtr3di	\|- ( z C_ ( B u. C ) -> z = ( ( z i^i B ) u. ( z i^i C ) ) )
58	57	inteqd	\|- ( z C_ ( B u. C ) -> \|^\| z = \|^\| ( ( z i^i B ) u. ( z i^i C ) ) )
59		intun	\|- \|^\| ( ( z i^i B ) u. ( z i^i C ) ) = ( \|^\| ( z i^i B ) i^i \|^\| ( z i^i C ) )
60	58 59	eqtrdi	\|- ( z C_ ( B u. C ) -> \|^\| z = ( \|^\| ( z i^i B ) i^i \|^\| ( z i^i C ) ) )
61	36 53 60	3syl	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> \|^\| z = ( \|^\| ( z i^i B ) i^i \|^\| ( z i^i C ) ) )
62		ineq1	\|- ( x = \|^\| ( z i^i B ) -> ( x i^i y ) = ( \|^\| ( z i^i B ) i^i y ) )
63	62	eqeq2d	\|- ( x = \|^\| ( z i^i B ) -> ( \|^\| z = ( x i^i y ) <-> \|^\| z = ( \|^\| ( z i^i B ) i^i y ) ) )
64		ineq2	\|- ( y = \|^\| ( z i^i C ) -> ( \|^\| ( z i^i B ) i^i y ) = ( \|^\| ( z i^i B ) i^i \|^\| ( z i^i C ) ) )
65	64	eqeq2d	\|- ( y = \|^\| ( z i^i C ) -> ( \|^\| z = ( \|^\| ( z i^i B ) i^i y ) <-> \|^\| z = ( \|^\| ( z i^i B ) i^i \|^\| ( z i^i C ) ) ) )
66	63 65	rspc2ev	\|- ( ( \|^\| ( z i^i B ) e. ( fi ` B ) /\ \|^\| ( z i^i C ) e. ( fi ` C ) /\ \|^\| z = ( \|^\| ( z i^i B ) i^i \|^\| ( z i^i C ) ) ) -> E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) )
67	42 51 61 66	syl3anc	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) )
68	67	3mix3d	\|- ( ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( \|^\| z e. ( fi ` B ) \/ \|^\| z e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) ) )
69	68	3expib	\|- ( ( ( z i^i B ) =/= (/) /\ ( z i^i C ) =/= (/) ) -> ( ( ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( \|^\| z e. ( fi ` B ) \/ \|^\| z e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) ) ) )
70		simp23	\|- ( ( ( z i^i B ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> C e. K )
71		simp1	\|- ( ( ( z i^i B ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( z i^i B ) = (/) )
72		simp3l	\|- ( ( ( z i^i B ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z e. ( ~P ( B u. C ) i^i Fin ) )
73		reldisj	\|- ( z C_ ( B u. C ) -> ( ( z i^i B ) = (/) <-> z C_ ( ( B u. C ) \ B ) ) )
74	72 53 73	3syl	\|- ( ( ( z i^i B ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( ( z i^i B ) = (/) <-> z C_ ( ( B u. C ) \ B ) ) )
75	71 74	mpbid	\|- ( ( ( z i^i B ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z C_ ( ( B u. C ) \ B ) )
76		uncom	\|- ( B u. C ) = ( C u. B )
77	76	difeq1i	\|- ( ( B u. C ) \ B ) = ( ( C u. B ) \ B )
78		difun2	\|- ( ( C u. B ) \ B ) = ( C \ B )
79	77 78	eqtri	\|- ( ( B u. C ) \ B ) = ( C \ B )
80		difss	\|- ( C \ B ) C_ C
81	79 80	eqsstri	\|- ( ( B u. C ) \ B ) C_ C
82	75 81	sstrdi	\|- ( ( ( z i^i B ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z C_ C )
83		simp3r	\|- ( ( ( z i^i B ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z =/= (/) )
84	72	elin2d	\|- ( ( ( z i^i B ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z e. Fin )
85		elfir	\|- ( ( C e. K /\ ( z C_ C /\ z =/= (/) /\ z e. Fin ) ) -> \|^\| z e. ( fi ` C ) )
86	70 82 83 84 85	syl13anc	\|- ( ( ( z i^i B ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> \|^\| z e. ( fi ` C ) )
87	86	3mix2d	\|- ( ( ( z i^i B ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( \|^\| z e. ( fi ` B ) \/ \|^\| z e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) ) )
88	87	3expib	\|- ( ( z i^i B ) = (/) -> ( ( ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( \|^\| z e. ( fi ` B ) \/ \|^\| z e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) ) ) )
89		simp22	\|- ( ( ( z i^i C ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> B e. D )
90		simp1	\|- ( ( ( z i^i C ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( z i^i C ) = (/) )
91		simp3l	\|- ( ( ( z i^i C ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z e. ( ~P ( B u. C ) i^i Fin ) )
92		reldisj	\|- ( z C_ ( B u. C ) -> ( ( z i^i C ) = (/) <-> z C_ ( ( B u. C ) \ C ) ) )
93	91 53 92	3syl	\|- ( ( ( z i^i C ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( ( z i^i C ) = (/) <-> z C_ ( ( B u. C ) \ C ) ) )
94	90 93	mpbid	\|- ( ( ( z i^i C ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z C_ ( ( B u. C ) \ C ) )
95		difun2	\|- ( ( B u. C ) \ C ) = ( B \ C )
96		difss	\|- ( B \ C ) C_ B
97	95 96	eqsstri	\|- ( ( B u. C ) \ C ) C_ B
98	94 97	sstrdi	\|- ( ( ( z i^i C ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z C_ B )
99		simp3r	\|- ( ( ( z i^i C ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z =/= (/) )
100	91	elin2d	\|- ( ( ( z i^i C ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> z e. Fin )
101		elfir	\|- ( ( B e. D /\ ( z C_ B /\ z =/= (/) /\ z e. Fin ) ) -> \|^\| z e. ( fi ` B ) )
102	89 98 99 100 101	syl13anc	\|- ( ( ( z i^i C ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> \|^\| z e. ( fi ` B ) )
103	102	3mix1d	\|- ( ( ( z i^i C ) = (/) /\ ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( \|^\| z e. ( fi ` B ) \/ \|^\| z e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) ) )
104	103	3expib	\|- ( ( z i^i C ) = (/) -> ( ( ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( \|^\| z e. ( fi ` B ) \/ \|^\| z e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) ) ) )
105	69 88 104	pm2.61iine	\|- ( ( ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( \|^\| z e. ( fi ` B ) \/ \|^\| z e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) ) )
106		eleq1	\|- ( A = \|^\| z -> ( A e. ( fi ` B ) <-> \|^\| z e. ( fi ` B ) ) )
107		eleq1	\|- ( A = \|^\| z -> ( A e. ( fi ` C ) <-> \|^\| z e. ( fi ` C ) ) )
108		eqeq1	\|- ( A = \|^\| z -> ( A = ( x i^i y ) <-> \|^\| z = ( x i^i y ) ) )
109	108	2rexbidv	\|- ( A = \|^\| z -> ( E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) <-> E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) ) )
110	106 107 109	3orbi123d	\|- ( A = \|^\| z -> ( ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) <-> ( \|^\| z e. ( fi ` B ) \/ \|^\| z e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) \|^\| z = ( x i^i y ) ) ) )
111	105 110	syl5ibrcom	\|- ( ( ( A e. _V /\ B e. D /\ C e. K ) /\ ( z e. ( ~P ( B u. C ) i^i Fin ) /\ z =/= (/) ) ) -> ( A = \|^\| z -> ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) )
112	111	expr	\|- ( ( ( A e. _V /\ B e. D /\ C e. K ) /\ z e. ( ~P ( B u. C ) i^i Fin ) ) -> ( z =/= (/) -> ( A = \|^\| z -> ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) ) )
113	112	com23	\|- ( ( ( A e. _V /\ B e. D /\ C e. K ) /\ z e. ( ~P ( B u. C ) i^i Fin ) ) -> ( A = \|^\| z -> ( z =/= (/) -> ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) ) )
114	31 113	mpdd	\|- ( ( ( A e. _V /\ B e. D /\ C e. K ) /\ z e. ( ~P ( B u. C ) i^i Fin ) ) -> ( A = \|^\| z -> ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) )
115	114	rexlimdva	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( E. z e. ( ~P ( B u. C ) i^i Fin ) A = \|^\| z -> ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) )
116	26 115	sylbid	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( A e. ( fi ` ( B u. C ) ) -> ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) )
117		ssun1	\|- B C_ ( B u. C )
118		fiss	\|- ( ( ( B u. C ) e. _V /\ B C_ ( B u. C ) ) -> ( fi ` B ) C_ ( fi ` ( B u. C ) ) )
119	23 117 118	sylancl	\|- ( ( B e. D /\ C e. K ) -> ( fi ` B ) C_ ( fi ` ( B u. C ) ) )
120	119	3adant1	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( fi ` B ) C_ ( fi ` ( B u. C ) ) )
121	120	sseld	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( A e. ( fi ` B ) -> A e. ( fi ` ( B u. C ) ) ) )
122		ssun2	\|- C C_ ( B u. C )
123		fiss	\|- ( ( ( B u. C ) e. _V /\ C C_ ( B u. C ) ) -> ( fi ` C ) C_ ( fi ` ( B u. C ) ) )
124	23 122 123	sylancl	\|- ( ( B e. D /\ C e. K ) -> ( fi ` C ) C_ ( fi ` ( B u. C ) ) )
125	124	3adant1	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( fi ` C ) C_ ( fi ` ( B u. C ) ) )
126	125	sseld	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( A e. ( fi ` C ) -> A e. ( fi ` ( B u. C ) ) ) )
127	120	sseld	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( x e. ( fi ` B ) -> x e. ( fi ` ( B u. C ) ) ) )
128	125	sseld	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( y e. ( fi ` C ) -> y e. ( fi ` ( B u. C ) ) ) )
129	127 128	anim12d	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( ( x e. ( fi ` B ) /\ y e. ( fi ` C ) ) -> ( x e. ( fi ` ( B u. C ) ) /\ y e. ( fi ` ( B u. C ) ) ) ) )
130		fiin	\|- ( ( x e. ( fi ` ( B u. C ) ) /\ y e. ( fi ` ( B u. C ) ) ) -> ( x i^i y ) e. ( fi ` ( B u. C ) ) )
131		eleq1a	\|- ( ( x i^i y ) e. ( fi ` ( B u. C ) ) -> ( A = ( x i^i y ) -> A e. ( fi ` ( B u. C ) ) ) )
132	130 131	syl	\|- ( ( x e. ( fi ` ( B u. C ) ) /\ y e. ( fi ` ( B u. C ) ) ) -> ( A = ( x i^i y ) -> A e. ( fi ` ( B u. C ) ) ) )
133	129 132	syl6	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( ( x e. ( fi ` B ) /\ y e. ( fi ` C ) ) -> ( A = ( x i^i y ) -> A e. ( fi ` ( B u. C ) ) ) ) )
134	133	rexlimdvv	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) -> A e. ( fi ` ( B u. C ) ) ) )
135	121 126 134	3jaod	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) -> A e. ( fi ` ( B u. C ) ) ) )
136	116 135	impbid	\|- ( ( A e. _V /\ B e. D /\ C e. K ) -> ( A e. ( fi ` ( B u. C ) ) <-> ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) )
137	5 21 136	pm5.21nd	\|- ( ( B e. D /\ C e. K ) -> ( A e. ( fi ` ( B u. C ) ) <-> ( A e. ( fi ` B ) \/ A e. ( fi ` C ) \/ E. x e. ( fi ` B ) E. y e. ( fi ` C ) A = ( x i^i y ) ) ) )

Metamath Proof Explorer

Theorem elfiun

Proof