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 ∈ D ∧ C ∈ K → A ∈ fi ⁡ B ∪ C ↔ A ∈ fi ⁡ B ∨ A ∈ fi ⁡ C ∨ ∃ x ∈ fi ⁡ B ∃ y ∈ fi ⁡ C A = x ∩ y

Proof

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