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 ( ( 𝐵𝐷𝐶𝐾 ) → ( 𝐴 ∈ ( fi ‘ ( 𝐵𝐶 ) ) ↔ ( 𝐴 ∈ ( fi ‘ 𝐵 ) ∨ 𝐴 ∈ ( fi ‘ 𝐶 ) ∨ ∃ 𝑥 ∈ ( fi ‘ 𝐵 ) ∃ 𝑦 ∈ ( fi ‘ 𝐶 ) 𝐴 = ( 𝑥𝑦 ) ) ) )

Proof

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