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 ‘ 𝐶 ) 𝐴 = ( 𝑥 ∩ 𝑦 ) ) ) ) |