Step |
Hyp |
Ref |
Expression |
1 |
|
alexsubALT.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
dfrex2 |
⊢ ( ∃ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = ∪ 𝑛 ↔ ¬ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) |
3 |
2
|
ralbii |
⊢ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = ∪ 𝑛 ↔ ∀ 𝑠 ∈ 𝑡 ¬ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) |
4 |
|
ralnex |
⊢ ( ∀ 𝑠 ∈ 𝑡 ¬ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ↔ ¬ ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) |
5 |
3 4
|
bitr2i |
⊢ ( ¬ ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ↔ ∀ 𝑠 ∈ 𝑡 ∃ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = ∪ 𝑛 ) |
6 |
|
elin |
⊢ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ↔ ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) ) |
7 |
|
elpwi |
⊢ ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) → 𝑛 ⊆ ( 𝑢 ∪ { 𝑠 } ) ) |
8 |
7
|
adantr |
⊢ ( ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) → 𝑛 ⊆ ( 𝑢 ∪ { 𝑠 } ) ) |
9 |
|
uncom |
⊢ ( 𝑢 ∪ { 𝑠 } ) = ( { 𝑠 } ∪ 𝑢 ) |
10 |
8 9
|
sseqtrdi |
⊢ ( ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) → 𝑛 ⊆ ( { 𝑠 } ∪ 𝑢 ) ) |
11 |
|
ssundif |
⊢ ( 𝑛 ⊆ ( { 𝑠 } ∪ 𝑢 ) ↔ ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ) |
12 |
10 11
|
sylib |
⊢ ( ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) → ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ) |
13 |
|
diffi |
⊢ ( 𝑛 ∈ Fin → ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) |
14 |
13
|
adantl |
⊢ ( ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) → ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) |
15 |
12 14
|
jca |
⊢ ( ( 𝑛 ∈ 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑛 ∈ Fin ) → ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) ) |
16 |
6 15
|
sylbi |
⊢ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) → ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) ) |
17 |
16
|
adantr |
⊢ ( ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) → ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) ) |
18 |
17
|
ad2antll |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) ) |
19 |
|
elin |
⊢ ( ( 𝑛 ∖ { 𝑠 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ↔ ( ( 𝑛 ∖ { 𝑠 } ) ∈ 𝒫 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) ) |
20 |
|
vex |
⊢ 𝑢 ∈ V |
21 |
20
|
elpw2 |
⊢ ( ( 𝑛 ∖ { 𝑠 } ) ∈ 𝒫 𝑢 ↔ ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ) |
22 |
21
|
anbi1i |
⊢ ( ( ( 𝑛 ∖ { 𝑠 } ) ∈ 𝒫 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) ↔ ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) ) |
23 |
19 22
|
bitr2i |
⊢ ( ( ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑢 ∧ ( 𝑛 ∖ { 𝑠 } ) ∈ Fin ) ↔ ( 𝑛 ∖ { 𝑠 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ) |
24 |
18 23
|
sylib |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ( 𝑛 ∖ { 𝑠 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ) |
25 |
|
simprrr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → 𝑋 = ∪ 𝑛 ) |
26 |
|
eldif |
⊢ ( 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ↔ ( 𝑥 ∈ 𝑛 ∧ ¬ 𝑥 ∈ { 𝑠 } ) ) |
27 |
26
|
simplbi2 |
⊢ ( 𝑥 ∈ 𝑛 → ( ¬ 𝑥 ∈ { 𝑠 } → 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) ) |
28 |
|
elun |
⊢ ( 𝑥 ∈ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) ↔ ( 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ∨ 𝑥 ∈ { 𝑠 } ) ) |
29 |
|
orcom |
⊢ ( ( 𝑥 ∈ { 𝑠 } ∨ 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) ↔ ( 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ∨ 𝑥 ∈ { 𝑠 } ) ) |
30 |
28 29
|
bitr4i |
⊢ ( 𝑥 ∈ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) ↔ ( 𝑥 ∈ { 𝑠 } ∨ 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) ) |
31 |
|
df-or |
⊢ ( ( 𝑥 ∈ { 𝑠 } ∨ 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) ↔ ( ¬ 𝑥 ∈ { 𝑠 } → 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) ) |
32 |
30 31
|
bitr2i |
⊢ ( ( ¬ 𝑥 ∈ { 𝑠 } → 𝑥 ∈ ( 𝑛 ∖ { 𝑠 } ) ) ↔ 𝑥 ∈ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) ) |
33 |
27 32
|
sylib |
⊢ ( 𝑥 ∈ 𝑛 → 𝑥 ∈ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) ) |
34 |
33
|
ssriv |
⊢ 𝑛 ⊆ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) |
35 |
|
uniss |
⊢ ( 𝑛 ⊆ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) → ∪ 𝑛 ⊆ ∪ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) ) |
36 |
34 35
|
mp1i |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ∪ 𝑛 ⊆ ∪ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) ) |
37 |
|
uniun |
⊢ ∪ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) = ( ∪ ( 𝑛 ∖ { 𝑠 } ) ∪ ∪ { 𝑠 } ) |
38 |
|
unisnv |
⊢ ∪ { 𝑠 } = 𝑠 |
39 |
38
|
uneq2i |
⊢ ( ∪ ( 𝑛 ∖ { 𝑠 } ) ∪ ∪ { 𝑠 } ) = ( ∪ ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) |
40 |
37 39
|
eqtri |
⊢ ∪ ( ( 𝑛 ∖ { 𝑠 } ) ∪ { 𝑠 } ) = ( ∪ ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) |
41 |
36 40
|
sseqtrdi |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ∪ 𝑛 ⊆ ( ∪ ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) ) |
42 |
25 41
|
eqsstrd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → 𝑋 ⊆ ( ∪ ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) ) |
43 |
|
difss |
⊢ ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑛 |
44 |
43
|
unissi |
⊢ ∪ ( 𝑛 ∖ { 𝑠 } ) ⊆ ∪ 𝑛 |
45 |
|
sseq2 |
⊢ ( 𝑋 = ∪ 𝑛 → ( ∪ ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑋 ↔ ∪ ( 𝑛 ∖ { 𝑠 } ) ⊆ ∪ 𝑛 ) ) |
46 |
44 45
|
mpbiri |
⊢ ( 𝑋 = ∪ 𝑛 → ∪ ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑋 ) |
47 |
46
|
adantl |
⊢ ( ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) → ∪ ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑋 ) |
48 |
47
|
ad2antll |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ∪ ( 𝑛 ∖ { 𝑠 } ) ⊆ 𝑋 ) |
49 |
|
elinel1 |
⊢ ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → 𝑡 ∈ 𝒫 𝑥 ) |
50 |
49
|
elpwid |
⊢ ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → 𝑡 ⊆ 𝑥 ) |
51 |
50
|
ad3antrrr |
⊢ ( ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) → 𝑡 ⊆ 𝑥 ) |
52 |
51
|
ad2antlr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → 𝑡 ⊆ 𝑥 ) |
53 |
|
simprl |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → 𝑠 ∈ 𝑡 ) |
54 |
52 53
|
sseldd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → 𝑠 ∈ 𝑥 ) |
55 |
|
elssuni |
⊢ ( 𝑠 ∈ 𝑥 → 𝑠 ⊆ ∪ 𝑥 ) |
56 |
54 55
|
syl |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → 𝑠 ⊆ ∪ 𝑥 ) |
57 |
|
fibas |
⊢ ( fi ‘ 𝑥 ) ∈ TopBases |
58 |
|
unitg |
⊢ ( ( fi ‘ 𝑥 ) ∈ TopBases → ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) = ∪ ( fi ‘ 𝑥 ) ) |
59 |
57 58
|
mp1i |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) = ∪ ( fi ‘ 𝑥 ) ) |
60 |
|
unieq |
⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ∪ 𝐽 = ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) ) |
61 |
60
|
3ad2ant1 |
⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ∪ 𝐽 = ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) ) |
62 |
61
|
ad3antrrr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ∪ 𝐽 = ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) ) |
63 |
|
vex |
⊢ 𝑥 ∈ V |
64 |
|
fiuni |
⊢ ( 𝑥 ∈ V → ∪ 𝑥 = ∪ ( fi ‘ 𝑥 ) ) |
65 |
63 64
|
mp1i |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ∪ 𝑥 = ∪ ( fi ‘ 𝑥 ) ) |
66 |
59 62 65
|
3eqtr4rd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ∪ 𝑥 = ∪ 𝐽 ) |
67 |
66 1
|
eqtr4di |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ∪ 𝑥 = 𝑋 ) |
68 |
56 67
|
sseqtrd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → 𝑠 ⊆ 𝑋 ) |
69 |
48 68
|
unssd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ( ∪ ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) ⊆ 𝑋 ) |
70 |
42 69
|
eqssd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → 𝑋 = ( ∪ ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) ) |
71 |
|
unieq |
⊢ ( 𝑚 = ( 𝑛 ∖ { 𝑠 } ) → ∪ 𝑚 = ∪ ( 𝑛 ∖ { 𝑠 } ) ) |
72 |
71
|
uneq1d |
⊢ ( 𝑚 = ( 𝑛 ∖ { 𝑠 } ) → ( ∪ 𝑚 ∪ 𝑠 ) = ( ∪ ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) ) |
73 |
72
|
rspceeqv |
⊢ ( ( ( 𝑛 ∖ { 𝑠 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑋 = ( ∪ ( 𝑛 ∖ { 𝑠 } ) ∪ 𝑠 ) ) → ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) ) |
74 |
24 70 73
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) ) ) → ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) ) |
75 |
74
|
expr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ 𝑠 ∈ 𝑡 ) → ( ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑛 ) → ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) ) ) |
76 |
75
|
expd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ 𝑠 ∈ 𝑡 ) → ( 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) → ( 𝑋 = ∪ 𝑛 → ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) ) ) ) |
77 |
76
|
rexlimdv |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ 𝑠 ∈ 𝑡 ) → ( ∃ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = ∪ 𝑛 → ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) ) ) |
78 |
77
|
ralimdva |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) → ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = ∪ 𝑛 → ∀ 𝑠 ∈ 𝑡 ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) ) ) |
79 |
|
elinel2 |
⊢ ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → 𝑡 ∈ Fin ) |
80 |
79
|
adantr |
⊢ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) → 𝑡 ∈ Fin ) |
81 |
|
unieq |
⊢ ( 𝑚 = ( 𝑓 ‘ 𝑠 ) → ∪ 𝑚 = ∪ ( 𝑓 ‘ 𝑠 ) ) |
82 |
81
|
uneq1d |
⊢ ( 𝑚 = ( 𝑓 ‘ 𝑠 ) → ( ∪ 𝑚 ∪ 𝑠 ) = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) |
83 |
82
|
eqeq2d |
⊢ ( 𝑚 = ( 𝑓 ‘ 𝑠 ) → ( 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) ↔ 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) |
84 |
83
|
ac6sfi |
⊢ ( ( 𝑡 ∈ Fin ∧ ∀ 𝑠 ∈ 𝑡 ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) |
85 |
84
|
ex |
⊢ ( 𝑡 ∈ Fin → ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) ) |
86 |
80 85
|
syl |
⊢ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) → ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) ) |
87 |
86
|
adantr |
⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) → ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) ) |
88 |
87
|
ad2antrl |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) → ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑚 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ( ∪ 𝑚 ∪ 𝑠 ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) ) |
89 |
|
ffvelcdm |
⊢ ( ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑠 ∈ 𝑡 ) → ( 𝑓 ‘ 𝑠 ) ∈ ( 𝒫 𝑢 ∩ Fin ) ) |
90 |
|
elin |
⊢ ( ( 𝑓 ‘ 𝑠 ) ∈ ( 𝒫 𝑢 ∩ Fin ) ↔ ( ( 𝑓 ‘ 𝑠 ) ∈ 𝒫 𝑢 ∧ ( 𝑓 ‘ 𝑠 ) ∈ Fin ) ) |
91 |
|
elpwi |
⊢ ( ( 𝑓 ‘ 𝑠 ) ∈ 𝒫 𝑢 → ( 𝑓 ‘ 𝑠 ) ⊆ 𝑢 ) |
92 |
91
|
adantr |
⊢ ( ( ( 𝑓 ‘ 𝑠 ) ∈ 𝒫 𝑢 ∧ ( 𝑓 ‘ 𝑠 ) ∈ Fin ) → ( 𝑓 ‘ 𝑠 ) ⊆ 𝑢 ) |
93 |
90 92
|
sylbi |
⊢ ( ( 𝑓 ‘ 𝑠 ) ∈ ( 𝒫 𝑢 ∩ Fin ) → ( 𝑓 ‘ 𝑠 ) ⊆ 𝑢 ) |
94 |
89 93
|
syl |
⊢ ( ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑠 ∈ 𝑡 ) → ( 𝑓 ‘ 𝑠 ) ⊆ 𝑢 ) |
95 |
94
|
ralrimiva |
⊢ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) → ∀ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ⊆ 𝑢 ) |
96 |
|
iunss |
⊢ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ⊆ 𝑢 ↔ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ⊆ 𝑢 ) |
97 |
95 96
|
sylibr |
⊢ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) → ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ⊆ 𝑢 ) |
98 |
97
|
ad2antrl |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ⊆ 𝑢 ) |
99 |
|
simplrr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → 𝑤 ∈ 𝑢 ) |
100 |
99
|
snssd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → { 𝑤 } ⊆ 𝑢 ) |
101 |
98 100
|
unssd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑢 ) |
102 |
89
|
elin2d |
⊢ ( ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑠 ∈ 𝑡 ) → ( 𝑓 ‘ 𝑠 ) ∈ Fin ) |
103 |
102
|
ralrimiva |
⊢ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) → ∀ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∈ Fin ) |
104 |
|
iunfi |
⊢ ( ( 𝑡 ∈ Fin ∧ ∀ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∈ Fin ) → ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∈ Fin ) |
105 |
80 103 104
|
syl2an |
⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ) → ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∈ Fin ) |
106 |
105
|
ad4ant14 |
⊢ ( ( ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ) → ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∈ Fin ) |
107 |
106
|
ad2ant2lr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∈ Fin ) |
108 |
|
snfi |
⊢ { 𝑤 } ∈ Fin |
109 |
|
unfi |
⊢ ( ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∈ Fin ∧ { 𝑤 } ∈ Fin ) → ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) |
110 |
107 108 109
|
sylancl |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) |
111 |
101 110
|
jca |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ( ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑢 ∧ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) ) |
112 |
|
elin |
⊢ ( ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ↔ ( ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ 𝒫 𝑢 ∧ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) ) |
113 |
20
|
elpw2 |
⊢ ( ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ 𝒫 𝑢 ↔ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑢 ) |
114 |
113
|
anbi1i |
⊢ ( ( ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ 𝒫 𝑢 ∧ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) ↔ ( ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑢 ∧ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) ) |
115 |
112 114
|
bitr2i |
⊢ ( ( ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑢 ∧ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ Fin ) ↔ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ) |
116 |
111 115
|
sylib |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ) |
117 |
|
ralnex |
⊢ ( ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ↔ ¬ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) |
118 |
117
|
imbi2i |
⊢ ( ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ↔ ( 𝑣 ∈ 𝑦 → ¬ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ) |
119 |
118
|
albii |
⊢ ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ↔ ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ¬ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ) |
120 |
|
alinexa |
⊢ ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ¬ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ↔ ¬ ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ) |
121 |
119 120
|
bitr2i |
⊢ ( ¬ ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ↔ ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ) |
122 |
|
fveq2 |
⊢ ( 𝑠 = 𝑧 → ( 𝑓 ‘ 𝑠 ) = ( 𝑓 ‘ 𝑧 ) ) |
123 |
122
|
unieqd |
⊢ ( 𝑠 = 𝑧 → ∪ ( 𝑓 ‘ 𝑠 ) = ∪ ( 𝑓 ‘ 𝑧 ) ) |
124 |
|
id |
⊢ ( 𝑠 = 𝑧 → 𝑠 = 𝑧 ) |
125 |
123 124
|
uneq12d |
⊢ ( 𝑠 = 𝑧 → ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) = ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) ) |
126 |
125
|
eqeq2d |
⊢ ( 𝑠 = 𝑧 → ( 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ↔ 𝑋 = ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) ) ) |
127 |
126
|
rspcv |
⊢ ( 𝑧 ∈ 𝑡 → ( ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) → 𝑋 = ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) ) ) |
128 |
|
eleq2 |
⊢ ( 𝑋 = ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) → ( 𝑣 ∈ 𝑋 ↔ 𝑣 ∈ ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) ) ) |
129 |
128
|
biimpd |
⊢ ( 𝑋 = ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) → ( 𝑣 ∈ 𝑋 → 𝑣 ∈ ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) ) ) |
130 |
|
elun |
⊢ ( 𝑣 ∈ ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) ↔ ( 𝑣 ∈ ∪ ( 𝑓 ‘ 𝑧 ) ∨ 𝑣 ∈ 𝑧 ) ) |
131 |
|
eluni |
⊢ ( 𝑣 ∈ ∪ ( 𝑓 ‘ 𝑧 ) ↔ ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ) |
132 |
131
|
orbi1i |
⊢ ( ( 𝑣 ∈ ∪ ( 𝑓 ‘ 𝑧 ) ∨ 𝑣 ∈ 𝑧 ) ↔ ( ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ∨ 𝑣 ∈ 𝑧 ) ) |
133 |
|
df-or |
⊢ ( ( ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ∨ 𝑣 ∈ 𝑧 ) ↔ ( ¬ ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) → 𝑣 ∈ 𝑧 ) ) |
134 |
|
alinexa |
⊢ ( ∀ 𝑤 ( 𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ↔ ¬ ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ) |
135 |
134
|
imbi1i |
⊢ ( ( ∀ 𝑤 ( 𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) → 𝑣 ∈ 𝑧 ) ↔ ( ¬ ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) → 𝑣 ∈ 𝑧 ) ) |
136 |
133 135
|
bitr4i |
⊢ ( ( ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ∨ 𝑣 ∈ 𝑧 ) ↔ ( ∀ 𝑤 ( 𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) → 𝑣 ∈ 𝑧 ) ) |
137 |
130 132 136
|
3bitri |
⊢ ( 𝑣 ∈ ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) ↔ ( ∀ 𝑤 ( 𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) → 𝑣 ∈ 𝑧 ) ) |
138 |
|
eleq2 |
⊢ ( 𝑦 = 𝑤 → ( 𝑣 ∈ 𝑦 ↔ 𝑣 ∈ 𝑤 ) ) |
139 |
|
eleq1w |
⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ↔ 𝑤 ∈ ( 𝑓 ‘ 𝑠 ) ) ) |
140 |
139
|
notbid |
⊢ ( 𝑦 = 𝑤 → ( ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ↔ ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑠 ) ) ) |
141 |
140
|
ralbidv |
⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝑡 ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑠 ) ) ) |
142 |
138 141
|
imbi12d |
⊢ ( 𝑦 = 𝑤 → ( ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ↔ ( 𝑣 ∈ 𝑤 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑠 ) ) ) ) |
143 |
142
|
spvv |
⊢ ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → ( 𝑣 ∈ 𝑤 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑠 ) ) ) |
144 |
122
|
eleq2d |
⊢ ( 𝑠 = 𝑧 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑠 ) ↔ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ) |
145 |
144
|
notbid |
⊢ ( 𝑠 = 𝑧 → ( ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑠 ) ↔ ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ) |
146 |
145
|
rspcv |
⊢ ( 𝑧 ∈ 𝑡 → ( ∀ 𝑠 ∈ 𝑡 ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑠 ) → ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ) |
147 |
143 146
|
syl9r |
⊢ ( 𝑧 ∈ 𝑡 → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → ( 𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ) ) |
148 |
147
|
alrimdv |
⊢ ( 𝑧 ∈ 𝑡 → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → ∀ 𝑤 ( 𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) ) ) |
149 |
148
|
imim1d |
⊢ ( 𝑧 ∈ 𝑡 → ( ( ∀ 𝑤 ( 𝑣 ∈ 𝑤 → ¬ 𝑤 ∈ ( 𝑓 ‘ 𝑧 ) ) → 𝑣 ∈ 𝑧 ) → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ 𝑧 ) ) ) |
150 |
137 149
|
biimtrid |
⊢ ( 𝑧 ∈ 𝑡 → ( 𝑣 ∈ ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ 𝑧 ) ) ) |
151 |
150
|
a1dd |
⊢ ( 𝑧 ∈ 𝑡 → ( 𝑣 ∈ ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) → ( 𝑤 = ∩ 𝑡 → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ 𝑧 ) ) ) ) |
152 |
129 151
|
syl9r |
⊢ ( 𝑧 ∈ 𝑡 → ( 𝑋 = ( ∪ ( 𝑓 ‘ 𝑧 ) ∪ 𝑧 ) → ( 𝑣 ∈ 𝑋 → ( 𝑤 = ∩ 𝑡 → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ 𝑧 ) ) ) ) ) |
153 |
127 152
|
syld |
⊢ ( 𝑧 ∈ 𝑡 → ( ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) → ( 𝑣 ∈ 𝑋 → ( 𝑤 = ∩ 𝑡 → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ 𝑧 ) ) ) ) ) |
154 |
153
|
com14 |
⊢ ( 𝑤 = ∩ 𝑡 → ( ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) → ( 𝑣 ∈ 𝑋 → ( 𝑧 ∈ 𝑡 → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ 𝑧 ) ) ) ) ) |
155 |
154
|
imp31 |
⊢ ( ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑡 → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ 𝑧 ) ) ) |
156 |
155
|
com23 |
⊢ ( ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣 ∈ 𝑋 ) → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → ( 𝑧 ∈ 𝑡 → 𝑣 ∈ 𝑧 ) ) ) |
157 |
156
|
ralrimdv |
⊢ ( ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣 ∈ 𝑋 ) → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → ∀ 𝑧 ∈ 𝑡 𝑣 ∈ 𝑧 ) ) |
158 |
|
vex |
⊢ 𝑣 ∈ V |
159 |
158
|
elint2 |
⊢ ( 𝑣 ∈ ∩ 𝑡 ↔ ∀ 𝑧 ∈ 𝑡 𝑣 ∈ 𝑧 ) |
160 |
157 159
|
syl6ibr |
⊢ ( ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣 ∈ 𝑋 ) → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ ∩ 𝑡 ) ) |
161 |
|
eleq2 |
⊢ ( 𝑤 = ∩ 𝑡 → ( 𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡 ) ) |
162 |
161
|
ad2antrr |
⊢ ( ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣 ∈ 𝑋 ) → ( 𝑣 ∈ 𝑤 ↔ 𝑣 ∈ ∩ 𝑡 ) ) |
163 |
160 162
|
sylibrd |
⊢ ( ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣 ∈ 𝑋 ) → ( ∀ 𝑦 ( 𝑣 ∈ 𝑦 → ∀ 𝑠 ∈ 𝑡 ¬ 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ 𝑤 ) ) |
164 |
121 163
|
biimtrid |
⊢ ( ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣 ∈ 𝑋 ) → ( ¬ ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → 𝑣 ∈ 𝑤 ) ) |
165 |
164
|
orrd |
⊢ ( ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ∧ 𝑣 ∈ 𝑋 ) → ( ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ∨ 𝑣 ∈ 𝑤 ) ) |
166 |
165
|
ex |
⊢ ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) → ( 𝑣 ∈ 𝑋 → ( ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ∨ 𝑣 ∈ 𝑤 ) ) ) |
167 |
|
orc |
⊢ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) → ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) |
168 |
167
|
anim2i |
⊢ ( ( 𝑣 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → ( 𝑣 ∈ 𝑦 ∧ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) ) |
169 |
168
|
eximi |
⊢ ( ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) → ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) ) |
170 |
|
equid |
⊢ 𝑤 = 𝑤 |
171 |
|
vex |
⊢ 𝑤 ∈ V |
172 |
|
equequ1 |
⊢ ( 𝑦 = 𝑤 → ( 𝑦 = 𝑤 ↔ 𝑤 = 𝑤 ) ) |
173 |
138 172
|
anbi12d |
⊢ ( 𝑦 = 𝑤 → ( ( 𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤 ) ↔ ( 𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤 ) ) ) |
174 |
171 173
|
spcev |
⊢ ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 = 𝑤 ) → ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤 ) ) |
175 |
170 174
|
mpan2 |
⊢ ( 𝑣 ∈ 𝑤 → ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤 ) ) |
176 |
|
olc |
⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) |
177 |
176
|
anim2i |
⊢ ( ( 𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤 ) → ( 𝑣 ∈ 𝑦 ∧ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) ) |
178 |
177
|
eximi |
⊢ ( ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ 𝑦 = 𝑤 ) → ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) ) |
179 |
175 178
|
syl |
⊢ ( 𝑣 ∈ 𝑤 → ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) ) |
180 |
169 179
|
jaoi |
⊢ ( ( ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ∨ 𝑣 ∈ 𝑤 ) → ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) ) |
181 |
|
eluni |
⊢ ( 𝑣 ∈ ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ↔ ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ∈ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) ) |
182 |
|
elun |
⊢ ( 𝑦 ∈ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ↔ ( 𝑦 ∈ ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 ∈ { 𝑤 } ) ) |
183 |
|
eliun |
⊢ ( 𝑦 ∈ ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ↔ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) |
184 |
|
velsn |
⊢ ( 𝑦 ∈ { 𝑤 } ↔ 𝑦 = 𝑤 ) |
185 |
183 184
|
orbi12i |
⊢ ( ( 𝑦 ∈ ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 ∈ { 𝑤 } ) ↔ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) |
186 |
182 185
|
bitri |
⊢ ( 𝑦 ∈ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ↔ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) |
187 |
186
|
anbi2i |
⊢ ( ( 𝑣 ∈ 𝑦 ∧ 𝑦 ∈ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) ↔ ( 𝑣 ∈ 𝑦 ∧ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) ) |
188 |
187
|
exbii |
⊢ ( ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ∈ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) ↔ ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) ) |
189 |
181 188
|
bitr2i |
⊢ ( ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ( ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑦 = 𝑤 ) ) ↔ 𝑣 ∈ ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) |
190 |
180 189
|
sylib |
⊢ ( ( ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝑡 𝑦 ∈ ( 𝑓 ‘ 𝑠 ) ) ∨ 𝑣 ∈ 𝑤 ) → 𝑣 ∈ ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) |
191 |
166 190
|
syl6 |
⊢ ( ( 𝑤 = ∩ 𝑡 ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) → ( 𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) ) |
192 |
191
|
ad5ant25 |
⊢ ( ( ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) → ( 𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) ) |
193 |
192
|
ad2ant2l |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ( 𝑣 ∈ 𝑋 → 𝑣 ∈ ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) ) |
194 |
193
|
ssrdv |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → 𝑋 ⊆ ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) |
195 |
|
elun |
⊢ ( 𝑣 ∈ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ↔ ( 𝑣 ∈ ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∨ 𝑣 ∈ { 𝑤 } ) ) |
196 |
|
eliun |
⊢ ( 𝑣 ∈ ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ↔ ∃ 𝑠 ∈ 𝑡 𝑣 ∈ ( 𝑓 ‘ 𝑠 ) ) |
197 |
|
velsn |
⊢ ( 𝑣 ∈ { 𝑤 } ↔ 𝑣 = 𝑤 ) |
198 |
196 197
|
orbi12i |
⊢ ( ( 𝑣 ∈ ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∨ 𝑣 ∈ { 𝑤 } ) ↔ ( ∃ 𝑠 ∈ 𝑡 𝑣 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑣 = 𝑤 ) ) |
199 |
195 198
|
bitri |
⊢ ( 𝑣 ∈ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ↔ ( ∃ 𝑠 ∈ 𝑡 𝑣 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑣 = 𝑤 ) ) |
200 |
|
nfra1 |
⊢ Ⅎ 𝑠 ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) |
201 |
|
nfv |
⊢ Ⅎ 𝑠 𝑣 ⊆ 𝑋 |
202 |
|
rsp |
⊢ ( ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) → ( 𝑠 ∈ 𝑡 → 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) |
203 |
|
eqimss2 |
⊢ ( 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) → ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ⊆ 𝑋 ) |
204 |
|
elssuni |
⊢ ( 𝑣 ∈ ( 𝑓 ‘ 𝑠 ) → 𝑣 ⊆ ∪ ( 𝑓 ‘ 𝑠 ) ) |
205 |
|
ssun3 |
⊢ ( 𝑣 ⊆ ∪ ( 𝑓 ‘ 𝑠 ) → 𝑣 ⊆ ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) |
206 |
204 205
|
syl |
⊢ ( 𝑣 ∈ ( 𝑓 ‘ 𝑠 ) → 𝑣 ⊆ ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) |
207 |
|
sstr |
⊢ ( ( 𝑣 ⊆ ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ∧ ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ⊆ 𝑋 ) → 𝑣 ⊆ 𝑋 ) |
208 |
207
|
expcom |
⊢ ( ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ⊆ 𝑋 → ( 𝑣 ⊆ ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) → 𝑣 ⊆ 𝑋 ) ) |
209 |
203 206 208
|
syl2im |
⊢ ( 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) → ( 𝑣 ∈ ( 𝑓 ‘ 𝑠 ) → 𝑣 ⊆ 𝑋 ) ) |
210 |
202 209
|
syl6 |
⊢ ( ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) → ( 𝑠 ∈ 𝑡 → ( 𝑣 ∈ ( 𝑓 ‘ 𝑠 ) → 𝑣 ⊆ 𝑋 ) ) ) |
211 |
200 201 210
|
rexlimd |
⊢ ( ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) → ( ∃ 𝑠 ∈ 𝑡 𝑣 ∈ ( 𝑓 ‘ 𝑠 ) → 𝑣 ⊆ 𝑋 ) ) |
212 |
211
|
ad2antll |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ( ∃ 𝑠 ∈ 𝑡 𝑣 ∈ ( 𝑓 ‘ 𝑠 ) → 𝑣 ⊆ 𝑋 ) ) |
213 |
|
elpwi |
⊢ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) ) |
214 |
213
|
ad2antrl |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) ) |
215 |
214
|
ad2antrr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) ) |
216 |
215 99
|
sseldd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → 𝑤 ∈ ( fi ‘ 𝑥 ) ) |
217 |
|
elssuni |
⊢ ( 𝑤 ∈ ( fi ‘ 𝑥 ) → 𝑤 ⊆ ∪ ( fi ‘ 𝑥 ) ) |
218 |
216 217
|
syl |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → 𝑤 ⊆ ∪ ( fi ‘ 𝑥 ) ) |
219 |
57 58
|
ax-mp |
⊢ ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) = ∪ ( fi ‘ 𝑥 ) |
220 |
60 219
|
eqtr2di |
⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ∪ ( fi ‘ 𝑥 ) = ∪ 𝐽 ) |
221 |
220 1
|
eqtr4di |
⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ∪ ( fi ‘ 𝑥 ) = 𝑋 ) |
222 |
221
|
3ad2ant1 |
⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ∪ ( fi ‘ 𝑥 ) = 𝑋 ) |
223 |
222
|
ad3antrrr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ∪ ( fi ‘ 𝑥 ) = 𝑋 ) |
224 |
218 223
|
sseqtrd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → 𝑤 ⊆ 𝑋 ) |
225 |
|
sseq1 |
⊢ ( 𝑣 = 𝑤 → ( 𝑣 ⊆ 𝑋 ↔ 𝑤 ⊆ 𝑋 ) ) |
226 |
224 225
|
syl5ibrcom |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ( 𝑣 = 𝑤 → 𝑣 ⊆ 𝑋 ) ) |
227 |
212 226
|
jaod |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ( ( ∃ 𝑠 ∈ 𝑡 𝑣 ∈ ( 𝑓 ‘ 𝑠 ) ∨ 𝑣 = 𝑤 ) → 𝑣 ⊆ 𝑋 ) ) |
228 |
199 227
|
biimtrid |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ( 𝑣 ∈ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) → 𝑣 ⊆ 𝑋 ) ) |
229 |
228
|
ralrimiv |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ∀ 𝑣 ∈ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) 𝑣 ⊆ 𝑋 ) |
230 |
|
unissb |
⊢ ( ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑋 ↔ ∀ 𝑣 ∈ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) 𝑣 ⊆ 𝑋 ) |
231 |
229 230
|
sylibr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ⊆ 𝑋 ) |
232 |
194 231
|
eqssd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → 𝑋 = ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) |
233 |
|
unieq |
⊢ ( 𝑏 = ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) → ∪ 𝑏 = ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) |
234 |
233
|
rspceeqv |
⊢ ( ( ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑋 = ∪ ( ∪ 𝑠 ∈ 𝑡 ( 𝑓 ‘ 𝑠 ) ∪ { 𝑤 } ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ) |
235 |
116 232 234
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) ∧ ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ) |
236 |
235
|
ex |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) → ( ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
237 |
236
|
exlimdv |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ ( 𝒫 𝑢 ∩ Fin ) ∧ ∀ 𝑠 ∈ 𝑡 𝑋 = ( ∪ ( 𝑓 ‘ 𝑠 ) ∪ 𝑠 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
238 |
78 88 237
|
3syld |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) → ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) 𝑋 = ∪ 𝑛 → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
239 |
5 238
|
biimtrid |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) → ( ¬ ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
240 |
|
dfrex2 |
⊢ ( ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ↔ ¬ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) |
241 |
239 240
|
imbitrdi |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) → ( ¬ ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 → ¬ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) |
242 |
241
|
con4d |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ) → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) |
243 |
242
|
exp32 |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) → ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) → ( 𝑤 ∈ 𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
244 |
243
|
com24 |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ 𝑎 ⊆ 𝑢 ) ) → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑤 ∈ 𝑢 → ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) → ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
245 |
244
|
exp32 |
⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) → ( 𝑎 ⊆ 𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑤 ∈ 𝑢 → ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) → ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) ) ) ) |
246 |
245
|
imp45 |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑤 ∈ 𝑢 → ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) → ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) |
247 |
246
|
imp31 |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) → ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) |