Step |
Hyp |
Ref |
Expression |
1 |
|
ptbas.1 |
⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } |
2 |
1
|
elpt |
⊢ ( 𝑋 ∈ 𝐵 ↔ ∃ 𝑎 ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ) ) |
3 |
1
|
elpt |
⊢ ( 𝑌 ∈ 𝐵 ↔ ∃ 𝑏 ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) |
4 |
2 3
|
anbi12i |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ↔ ( ∃ 𝑎 ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ) ∧ ∃ 𝑏 ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) ) |
5 |
|
exdistrv |
⊢ ( ∃ 𝑎 ∃ 𝑏 ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) ↔ ( ∃ 𝑎 ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ) ∧ ∃ 𝑏 ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) ) |
6 |
4 5
|
bitr4i |
⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) ) |
7 |
|
an4 |
⊢ ( ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) ) |
8 |
|
an6 |
⊢ ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) |
9 |
|
df-3an |
⊢ ( ( ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ∧ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) |
10 |
8 9
|
bitri |
⊢ ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) |
11 |
|
reeanv |
⊢ ( ∃ 𝑐 ∈ Fin ∃ 𝑑 ∈ Fin ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ↔ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) |
12 |
|
fveq2 |
⊢ ( 𝑦 = 𝑘 → ( 𝑎 ‘ 𝑦 ) = ( 𝑎 ‘ 𝑘 ) ) |
13 |
|
fveq2 |
⊢ ( 𝑦 = 𝑘 → ( 𝑏 ‘ 𝑦 ) = ( 𝑏 ‘ 𝑘 ) ) |
14 |
12 13
|
ineq12d |
⊢ ( 𝑦 = 𝑘 → ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) = ( ( 𝑎 ‘ 𝑘 ) ∩ ( 𝑏 ‘ 𝑘 ) ) ) |
15 |
14
|
cbvixpv |
⊢ X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) = X 𝑘 ∈ 𝐴 ( ( 𝑎 ‘ 𝑘 ) ∩ ( 𝑏 ‘ 𝑘 ) ) |
16 |
|
simpl1l |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐴 ∈ 𝑉 ) |
17 |
|
unfi |
⊢ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) → ( 𝑐 ∪ 𝑑 ) ∈ Fin ) |
18 |
17
|
ad2antrl |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( 𝑐 ∪ 𝑑 ) ∈ Fin ) |
19 |
|
simpl1r |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝐹 : 𝐴 ⟶ Top ) |
20 |
19
|
ffvelrnda |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ Top ) |
21 |
|
simpl3l |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) |
22 |
|
fveq2 |
⊢ ( 𝑦 = 𝑘 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑘 ) ) |
23 |
12 22
|
eleq12d |
⊢ ( 𝑦 = 𝑘 → ( ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑎 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) ) |
24 |
23
|
rspccva |
⊢ ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑎 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) |
25 |
21 24
|
sylan |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑎 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) |
26 |
|
simpl3r |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) |
27 |
13 22
|
eleq12d |
⊢ ( 𝑦 = 𝑘 → ( ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) ) |
28 |
27
|
rspccva |
⊢ ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑏 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) |
29 |
26 28
|
sylan |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑏 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) |
30 |
|
inopn |
⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ Top ∧ ( 𝑎 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ∧ ( 𝑏 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑎 ‘ 𝑘 ) ∩ ( 𝑏 ‘ 𝑘 ) ) ∈ ( 𝐹 ‘ 𝑘 ) ) |
31 |
20 25 29 30
|
syl3anc |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑎 ‘ 𝑘 ) ∩ ( 𝑏 ‘ 𝑘 ) ) ∈ ( 𝐹 ‘ 𝑘 ) ) |
32 |
|
simprrl |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) |
33 |
|
ssun1 |
⊢ 𝑐 ⊆ ( 𝑐 ∪ 𝑑 ) |
34 |
|
sscon |
⊢ ( 𝑐 ⊆ ( 𝑐 ∪ 𝑑 ) → ( 𝐴 ∖ ( 𝑐 ∪ 𝑑 ) ) ⊆ ( 𝐴 ∖ 𝑐 ) ) |
35 |
33 34
|
ax-mp |
⊢ ( 𝐴 ∖ ( 𝑐 ∪ 𝑑 ) ) ⊆ ( 𝐴 ∖ 𝑐 ) |
36 |
35
|
sseli |
⊢ ( 𝑘 ∈ ( 𝐴 ∖ ( 𝑐 ∪ 𝑑 ) ) → 𝑘 ∈ ( 𝐴 ∖ 𝑐 ) ) |
37 |
22
|
unieqd |
⊢ ( 𝑦 = 𝑘 → ∪ ( 𝐹 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) |
38 |
12 37
|
eqeq12d |
⊢ ( 𝑦 = 𝑘 → ( ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑎 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) ) |
39 |
38
|
rspccva |
⊢ ( ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑐 ) ) → ( 𝑎 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) |
40 |
32 36 39
|
syl2an |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝑐 ∪ 𝑑 ) ) ) → ( 𝑎 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) |
41 |
|
simprrr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) |
42 |
|
ssun2 |
⊢ 𝑑 ⊆ ( 𝑐 ∪ 𝑑 ) |
43 |
|
sscon |
⊢ ( 𝑑 ⊆ ( 𝑐 ∪ 𝑑 ) → ( 𝐴 ∖ ( 𝑐 ∪ 𝑑 ) ) ⊆ ( 𝐴 ∖ 𝑑 ) ) |
44 |
42 43
|
ax-mp |
⊢ ( 𝐴 ∖ ( 𝑐 ∪ 𝑑 ) ) ⊆ ( 𝐴 ∖ 𝑑 ) |
45 |
44
|
sseli |
⊢ ( 𝑘 ∈ ( 𝐴 ∖ ( 𝑐 ∪ 𝑑 ) ) → 𝑘 ∈ ( 𝐴 ∖ 𝑑 ) ) |
46 |
13 37
|
eqeq12d |
⊢ ( 𝑦 = 𝑘 → ( ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑏 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) ) |
47 |
46
|
rspccva |
⊢ ( ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑑 ) ) → ( 𝑏 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) |
48 |
41 45 47
|
syl2an |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝑐 ∪ 𝑑 ) ) ) → ( 𝑏 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) ) |
49 |
40 48
|
ineq12d |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝑐 ∪ 𝑑 ) ) ) → ( ( 𝑎 ‘ 𝑘 ) ∩ ( 𝑏 ‘ 𝑘 ) ) = ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ ∪ ( 𝐹 ‘ 𝑘 ) ) ) |
50 |
|
inidm |
⊢ ( ∪ ( 𝐹 ‘ 𝑘 ) ∩ ∪ ( 𝐹 ‘ 𝑘 ) ) = ∪ ( 𝐹 ‘ 𝑘 ) |
51 |
49 50
|
eqtrdi |
⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝑐 ∪ 𝑑 ) ) ) → ( ( 𝑎 ‘ 𝑘 ) ∩ ( 𝑏 ‘ 𝑘 ) ) = ∪ ( 𝐹 ‘ 𝑘 ) ) |
52 |
1 16 18 31 51
|
elptr2 |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → X 𝑘 ∈ 𝐴 ( ( 𝑎 ‘ 𝑘 ) ∩ ( 𝑏 ‘ 𝑘 ) ) ∈ 𝐵 ) |
53 |
15 52
|
eqeltrid |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) ∈ 𝐵 ) |
54 |
53
|
expr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑐 ∈ Fin ∧ 𝑑 ∈ Fin ) ) → ( ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) → X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) ∈ 𝐵 ) ) |
55 |
54
|
rexlimdvva |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) → ( ∃ 𝑐 ∈ Fin ∃ 𝑑 ∈ Fin ( ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) → X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) ∈ 𝐵 ) ) |
56 |
11 55
|
syl5bir |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) → ( ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) → X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) ∈ 𝐵 ) ) |
57 |
56
|
3expb |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) → X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) ∈ 𝐵 ) ) |
58 |
57
|
impr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( ( ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) ∧ ( ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) ∈ 𝐵 ) |
59 |
10 58
|
sylan2b |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) ∈ 𝐵 ) |
60 |
|
ineq12 |
⊢ ( ( 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) → ( 𝑋 ∩ 𝑌 ) = ( X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∩ X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) |
61 |
|
ixpin |
⊢ X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) = ( X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∩ X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) |
62 |
60 61
|
eqtr4di |
⊢ ( ( 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) → ( 𝑋 ∩ 𝑌 ) = X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) ) |
63 |
62
|
eleq1d |
⊢ ( ( 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) → ( ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 ↔ X 𝑦 ∈ 𝐴 ( ( 𝑎 ‘ 𝑦 ) ∩ ( 𝑏 ‘ 𝑦 ) ) ∈ 𝐵 ) ) |
64 |
59 63
|
syl5ibrcom |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ( 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 ) ) |
65 |
64
|
expimpd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 ) ) |
66 |
7 65
|
syl5bi |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 ) ) |
67 |
66
|
exlimdvv |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ∃ 𝑎 ∃ 𝑏 ( ( ( 𝑎 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑐 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑐 ) ( 𝑎 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑋 = X 𝑦 ∈ 𝐴 ( 𝑎 ‘ 𝑦 ) ) ∧ ( ( 𝑏 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ∈ ( 𝐹 ‘ 𝑦 ) ∧ ∃ 𝑑 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑑 ) ( 𝑏 ‘ 𝑦 ) = ∪ ( 𝐹 ‘ 𝑦 ) ) ∧ 𝑌 = X 𝑦 ∈ 𝐴 ( 𝑏 ‘ 𝑦 ) ) ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 ) ) |
68 |
6 67
|
syl5bi |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 ) ) |
69 |
68
|
imp |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∩ 𝑌 ) ∈ 𝐵 ) |