Step |
Hyp |
Ref |
Expression |
1 |
|
funmpt |
⊢ Fun ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) |
2 |
|
funiunfv |
⊢ ( Fun ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) → ∪ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) ‘ 𝑐 ) = ∪ ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ) |
3 |
1 2
|
mp1i |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ∪ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) ‘ 𝑐 ) = ∪ ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ) |
4 |
|
elinel1 |
⊢ ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝑐 ∈ 𝒫 𝑎 ) |
5 |
4
|
elpwid |
⊢ ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝑐 ⊆ 𝑎 ) |
6 |
|
elpwi |
⊢ ( 𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋 ) |
7 |
5 6
|
sylan9ssr |
⊢ ( ( 𝑎 ∈ 𝒫 𝑋 ∧ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ) → 𝑐 ⊆ 𝑋 ) |
8 |
|
velpw |
⊢ ( 𝑐 ∈ 𝒫 𝑋 ↔ 𝑐 ⊆ 𝑋 ) |
9 |
7 8
|
sylibr |
⊢ ( ( 𝑎 ∈ 𝒫 𝑋 ∧ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ) → 𝑐 ∈ 𝒫 𝑋 ) |
10 |
9
|
adantll |
⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ) → 𝑐 ∈ 𝒫 𝑋 ) |
11 |
|
eqeq1 |
⊢ ( 𝑏 = 𝑐 → ( 𝑏 = 𝑇 ↔ 𝑐 = 𝑇 ) ) |
12 |
11
|
ifbid |
⊢ ( 𝑏 = 𝑐 → if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ) |
13 |
|
eqid |
⊢ ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) = ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) |
14 |
|
snex |
⊢ { 𝐾 } ∈ V |
15 |
|
0ex |
⊢ ∅ ∈ V |
16 |
14 15
|
ifex |
⊢ if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ∈ V |
17 |
12 13 16
|
fvmpt |
⊢ ( 𝑐 ∈ 𝒫 𝑋 → ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) ‘ 𝑐 ) = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ) |
18 |
10 17
|
syl |
⊢ ( ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) ∧ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ) → ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) ‘ 𝑐 ) = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ) |
19 |
18
|
iuneq2dv |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ∪ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) ‘ 𝑐 ) = ∪ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ) |
20 |
3 19
|
eqtr3d |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ∪ ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) = ∪ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ) |
21 |
20
|
sseq1d |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∪ ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 ↔ ∪ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ) ) |
22 |
|
iunss |
⊢ ( ∪ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ) |
23 |
|
sseq1 |
⊢ ( { 𝐾 } = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) → ( { 𝐾 } ⊆ 𝑎 ↔ if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ) ) |
24 |
23
|
bibi1d |
⊢ ( { 𝐾 } = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) → ( ( { 𝐾 } ⊆ 𝑎 ↔ ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ↔ ( if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) ) |
25 |
|
sseq1 |
⊢ ( ∅ = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) → ( ∅ ⊆ 𝑎 ↔ if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ) ) |
26 |
25
|
bibi1d |
⊢ ( ∅ = if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) → ( ( ∅ ⊆ 𝑎 ↔ ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ↔ ( if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) ) |
27 |
|
snssg |
⊢ ( 𝐾 ∈ 𝑋 → ( 𝐾 ∈ 𝑎 ↔ { 𝐾 } ⊆ 𝑎 ) ) |
28 |
27
|
adantr |
⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑐 = 𝑇 ) → ( 𝐾 ∈ 𝑎 ↔ { 𝐾 } ⊆ 𝑎 ) ) |
29 |
|
biimt |
⊢ ( 𝑐 = 𝑇 → ( 𝐾 ∈ 𝑎 ↔ ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) |
30 |
29
|
adantl |
⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑐 = 𝑇 ) → ( 𝐾 ∈ 𝑎 ↔ ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) |
31 |
28 30
|
bitr3d |
⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑐 = 𝑇 ) → ( { 𝐾 } ⊆ 𝑎 ↔ ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) |
32 |
|
0ss |
⊢ ∅ ⊆ 𝑎 |
33 |
32
|
a1i |
⊢ ( ¬ 𝑐 = 𝑇 → ∅ ⊆ 𝑎 ) |
34 |
|
pm2.21 |
⊢ ( ¬ 𝑐 = 𝑇 → ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) |
35 |
33 34
|
2thd |
⊢ ( ¬ 𝑐 = 𝑇 → ( ∅ ⊆ 𝑎 ↔ ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) |
36 |
35
|
adantl |
⊢ ( ( 𝐾 ∈ 𝑋 ∧ ¬ 𝑐 = 𝑇 ) → ( ∅ ⊆ 𝑎 ↔ ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) |
37 |
24 26 31 36
|
ifbothda |
⊢ ( 𝐾 ∈ 𝑋 → ( if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) |
38 |
37
|
ralbidv |
⊢ ( 𝐾 ∈ 𝑋 → ( ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) |
39 |
38
|
ad3antlr |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) |
40 |
22 39
|
syl5bb |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∪ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) if ( 𝑐 = 𝑇 , { 𝐾 } , ∅ ) ⊆ 𝑎 ↔ ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) |
41 |
|
inss1 |
⊢ ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑎 |
42 |
6
|
sspwd |
⊢ ( 𝑎 ∈ 𝒫 𝑋 → 𝒫 𝑎 ⊆ 𝒫 𝑋 ) |
43 |
41 42
|
sstrid |
⊢ ( 𝑎 ∈ 𝒫 𝑋 → ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑋 ) |
44 |
43
|
adantl |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑋 ) |
45 |
|
ralss |
⊢ ( ( 𝒫 𝑎 ∩ Fin ) ⊆ 𝒫 𝑋 → ( ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ↔ ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) ) |
46 |
44 45
|
syl |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ↔ ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ) ) |
47 |
|
bi2.04 |
⊢ ( ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ↔ ( 𝑐 = 𝑇 → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾 ∈ 𝑎 ) ) ) |
48 |
47
|
ralbii |
⊢ ( ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ↔ ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 = 𝑇 → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾 ∈ 𝑎 ) ) ) |
49 |
|
elpwg |
⊢ ( 𝑇 ∈ Fin → ( 𝑇 ∈ 𝒫 𝑋 ↔ 𝑇 ⊆ 𝑋 ) ) |
50 |
49
|
biimparc |
⊢ ( ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) → 𝑇 ∈ 𝒫 𝑋 ) |
51 |
50
|
ad2antlr |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑇 ∈ 𝒫 𝑋 ) |
52 |
|
eleq1 |
⊢ ( 𝑐 = 𝑇 → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ↔ 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) ) ) |
53 |
52
|
imbi1d |
⊢ ( 𝑐 = 𝑇 → ( ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾 ∈ 𝑎 ) ↔ ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾 ∈ 𝑎 ) ) ) |
54 |
53
|
ceqsralv |
⊢ ( 𝑇 ∈ 𝒫 𝑋 → ( ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 = 𝑇 → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾 ∈ 𝑎 ) ) ↔ ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾 ∈ 𝑎 ) ) ) |
55 |
51 54
|
syl |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 = 𝑇 → ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾 ∈ 𝑎 ) ) ↔ ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾 ∈ 𝑎 ) ) ) |
56 |
48 55
|
syl5bb |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑐 ∈ 𝒫 𝑋 ( 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) → ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ) ↔ ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾 ∈ 𝑎 ) ) ) |
57 |
|
simplrr |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → 𝑇 ∈ Fin ) |
58 |
57
|
biantrud |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑇 ∈ 𝒫 𝑎 ↔ ( 𝑇 ∈ 𝒫 𝑎 ∧ 𝑇 ∈ Fin ) ) ) |
59 |
|
elin |
⊢ ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) ↔ ( 𝑇 ∈ 𝒫 𝑎 ∧ 𝑇 ∈ Fin ) ) |
60 |
58 59
|
bitr4di |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑇 ∈ 𝒫 𝑎 ↔ 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) ) ) |
61 |
|
vex |
⊢ 𝑎 ∈ V |
62 |
61
|
elpw2 |
⊢ ( 𝑇 ∈ 𝒫 𝑎 ↔ 𝑇 ⊆ 𝑎 ) |
63 |
60 62
|
bitr3di |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) ↔ 𝑇 ⊆ 𝑎 ) ) |
64 |
63
|
imbi1d |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑇 ∈ ( 𝒫 𝑎 ∩ Fin ) → 𝐾 ∈ 𝑎 ) ↔ ( 𝑇 ⊆ 𝑎 → 𝐾 ∈ 𝑎 ) ) ) |
65 |
46 56 64
|
3bitrd |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ∀ 𝑐 ∈ ( 𝒫 𝑎 ∩ Fin ) ( 𝑐 = 𝑇 → 𝐾 ∈ 𝑎 ) ↔ ( 𝑇 ⊆ 𝑎 → 𝐾 ∈ 𝑎 ) ) ) |
66 |
21 40 65
|
3bitrrd |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑎 ∈ 𝒫 𝑋 ) → ( ( 𝑇 ⊆ 𝑎 → 𝐾 ∈ 𝑎 ) ↔ ∪ ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 ) ) |
67 |
66
|
rabbidva |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( 𝑇 ⊆ 𝑎 → 𝐾 ∈ 𝑎 ) } = { 𝑎 ∈ 𝒫 𝑋 ∣ ∪ ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 } ) |
68 |
|
simpll |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) → 𝑋 ∈ 𝑉 ) |
69 |
|
snelpwi |
⊢ ( 𝐾 ∈ 𝑋 → { 𝐾 } ∈ 𝒫 𝑋 ) |
70 |
69
|
ad2antlr |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) → { 𝐾 } ∈ 𝒫 𝑋 ) |
71 |
|
0elpw |
⊢ ∅ ∈ 𝒫 𝑋 |
72 |
|
ifcl |
⊢ ( ( { 𝐾 } ∈ 𝒫 𝑋 ∧ ∅ ∈ 𝒫 𝑋 ) → if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ∈ 𝒫 𝑋 ) |
73 |
70 71 72
|
sylancl |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) → if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ∈ 𝒫 𝑋 ) |
74 |
73
|
adantr |
⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) ∧ 𝑏 ∈ 𝒫 𝑋 ) → if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ∈ 𝒫 𝑋 ) |
75 |
74
|
fmpttd |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) → ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) |
76 |
|
isacs1i |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) : 𝒫 𝑋 ⟶ 𝒫 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∪ ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 } ∈ ( ACS ‘ 𝑋 ) ) |
77 |
68 75 76
|
syl2anc |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∪ ( ( 𝑏 ∈ 𝒫 𝑋 ↦ if ( 𝑏 = 𝑇 , { 𝐾 } , ∅ ) ) “ ( 𝒫 𝑎 ∩ Fin ) ) ⊆ 𝑎 } ∈ ( ACS ‘ 𝑋 ) ) |
78 |
67 77
|
eqeltrd |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( 𝑇 ⊆ 𝑋 ∧ 𝑇 ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( 𝑇 ⊆ 𝑎 → 𝐾 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) ) |