Metamath Proof Explorer

Theorem 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 df-ss 
 |-  ( 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 ) ) ) )