This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 dfss2 ⊢ ( 𝑧 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑧 ∩ ( 𝐵 ∪ 𝐶 ) ) = 𝑧 )
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 ‘ 𝐶 ) 𝐴 = ( 𝑥 ∩ 𝑦 ) ) ) )