| Step |
Hyp |
Ref |
Expression |
| 1 |
|
inass |
⊢ ( ( 𝐴 ∩ 𝐾 ) ∩ ∪ 𝐽 ) = ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) |
| 2 |
|
in32 |
⊢ ( ( 𝐴 ∩ 𝐾 ) ∩ ∪ 𝐽 ) = ( ( 𝐴 ∩ ∪ 𝐽 ) ∩ 𝐾 ) |
| 3 |
1 2
|
eqtr3i |
⊢ ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) = ( ( 𝐴 ∩ ∪ 𝐽 ) ∩ 𝐾 ) |
| 4 |
|
df-kgen |
⊢ 𝑘Gen = ( 𝑗 ∈ Top ↦ { 𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀ 𝑦 ∈ 𝒫 ∪ 𝑗 ( ( 𝑗 ↾t 𝑦 ) ∈ Comp → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝑗 ↾t 𝑦 ) ) } ) |
| 5 |
4
|
mptrcl |
⊢ ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) → 𝐽 ∈ Top ) |
| 6 |
5
|
adantr |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐽 ∈ Top ) |
| 7 |
|
toptopon2 |
⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
| 8 |
6 7
|
sylib |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
| 9 |
|
simpl |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ) |
| 10 |
|
elkgen |
⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ↔ ( 𝐴 ⊆ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ) ) ) |
| 11 |
10
|
biimpa |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ) → ( 𝐴 ⊆ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ) ) |
| 12 |
8 9 11
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ⊆ ∪ 𝐽 ∧ ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ) ) |
| 13 |
12
|
simpld |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐴 ⊆ ∪ 𝐽 ) |
| 14 |
|
df-ss |
⊢ ( 𝐴 ⊆ ∪ 𝐽 ↔ ( 𝐴 ∩ ∪ 𝐽 ) = 𝐴 ) |
| 15 |
13 14
|
sylib |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ ∪ 𝐽 ) = 𝐴 ) |
| 16 |
15
|
ineq1d |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( ( 𝐴 ∩ ∪ 𝐽 ) ∩ 𝐾 ) = ( 𝐴 ∩ 𝐾 ) ) |
| 17 |
3 16
|
syl5eq |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) = ( 𝐴 ∩ 𝐾 ) ) |
| 18 |
|
cmptop |
⊢ ( ( 𝐽 ↾t 𝐾 ) ∈ Comp → ( 𝐽 ↾t 𝐾 ) ∈ Top ) |
| 19 |
18
|
adantl |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ∈ Top ) |
| 20 |
|
restrcl |
⊢ ( ( 𝐽 ↾t 𝐾 ) ∈ Top → ( 𝐽 ∈ V ∧ 𝐾 ∈ V ) ) |
| 21 |
20
|
simprd |
⊢ ( ( 𝐽 ↾t 𝐾 ) ∈ Top → 𝐾 ∈ V ) |
| 22 |
19 21
|
syl |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → 𝐾 ∈ V ) |
| 23 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
| 24 |
23
|
restin |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ V ) → ( 𝐽 ↾t 𝐾 ) = ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) |
| 25 |
6 22 24
|
syl2anc |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) = ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) |
| 26 |
|
simpr |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t 𝐾 ) ∈ Comp ) |
| 27 |
25 26
|
eqeltrrd |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ Comp ) |
| 28 |
|
oveq2 |
⊢ ( 𝑦 = ( 𝐾 ∩ ∪ 𝐽 ) → ( 𝐽 ↾t 𝑦 ) = ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) |
| 29 |
28
|
eleq1d |
⊢ ( 𝑦 = ( 𝐾 ∩ ∪ 𝐽 ) → ( ( 𝐽 ↾t 𝑦 ) ∈ Comp ↔ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ Comp ) ) |
| 30 |
|
ineq2 |
⊢ ( 𝑦 = ( 𝐾 ∩ ∪ 𝐽 ) → ( 𝐴 ∩ 𝑦 ) = ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) ) |
| 31 |
30 28
|
eleq12d |
⊢ ( 𝑦 = ( 𝐾 ∩ ∪ 𝐽 ) → ( ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ↔ ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) ) |
| 32 |
29 31
|
imbi12d |
⊢ ( 𝑦 = ( 𝐾 ∩ ∪ 𝐽 ) → ( ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ↔ ( ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ Comp → ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) ) ) |
| 33 |
12
|
simprd |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ∀ 𝑦 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑦 ) ∈ Comp → ( 𝐴 ∩ 𝑦 ) ∈ ( 𝐽 ↾t 𝑦 ) ) ) |
| 34 |
|
inss2 |
⊢ ( 𝐾 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 |
| 35 |
|
inex1g |
⊢ ( 𝐾 ∈ V → ( 𝐾 ∩ ∪ 𝐽 ) ∈ V ) |
| 36 |
|
elpwg |
⊢ ( ( 𝐾 ∩ ∪ 𝐽 ) ∈ V → ( ( 𝐾 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ↔ ( 𝐾 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) ) |
| 37 |
22 35 36
|
3syl |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( ( 𝐾 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ↔ ( 𝐾 ∩ ∪ 𝐽 ) ⊆ ∪ 𝐽 ) ) |
| 38 |
34 37
|
mpbiri |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐾 ∩ ∪ 𝐽 ) ∈ 𝒫 ∪ 𝐽 ) |
| 39 |
32 33 38
|
rspcdva |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ Comp → ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) ) |
| 40 |
27 39
|
mpd |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ ( 𝐾 ∩ ∪ 𝐽 ) ) ∈ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) |
| 41 |
17 40
|
eqeltrrd |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ 𝐾 ) ∈ ( 𝐽 ↾t ( 𝐾 ∩ ∪ 𝐽 ) ) ) |
| 42 |
41 25
|
eleqtrrd |
⊢ ( ( 𝐴 ∈ ( 𝑘Gen ‘ 𝐽 ) ∧ ( 𝐽 ↾t 𝐾 ) ∈ Comp ) → ( 𝐴 ∩ 𝐾 ) ∈ ( 𝐽 ↾t 𝐾 ) ) |