Step |
Hyp |
Ref |
Expression |
1 |
|
alexsubALT.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
ralnex |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ¬ ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) |
3 |
1
|
alexsubALTlem2 |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ∃ 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 ) |
4 |
|
elun |
⊢ ( 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ↔ ( 𝑢 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∨ 𝑢 ∈ { ∅ } ) ) |
5 |
|
sseq2 |
⊢ ( 𝑧 = 𝑢 → ( 𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑢 ) ) |
6 |
|
pweq |
⊢ ( 𝑧 = 𝑢 → 𝒫 𝑧 = 𝒫 𝑢 ) |
7 |
6
|
ineq1d |
⊢ ( 𝑧 = 𝑢 → ( 𝒫 𝑧 ∩ Fin ) = ( 𝒫 𝑢 ∩ Fin ) ) |
8 |
7
|
raleqdv |
⊢ ( 𝑧 = 𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) |
9 |
5 8
|
anbi12d |
⊢ ( 𝑧 = 𝑢 → ( ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ↔ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
10 |
9
|
elrab |
⊢ ( 𝑢 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ↔ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
11 |
|
velsn |
⊢ ( 𝑢 ∈ { ∅ } ↔ 𝑢 = ∅ ) |
12 |
10 11
|
orbi12i |
⊢ ( ( 𝑢 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∨ 𝑢 ∈ { ∅ } ) ↔ ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ∨ 𝑢 = ∅ ) ) |
13 |
4 12
|
bitri |
⊢ ( 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ↔ ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ∨ 𝑢 = ∅ ) ) |
14 |
|
ralnex |
⊢ ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 ↔ ¬ ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) |
15 |
|
simprrl |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → 𝑎 ⊆ 𝑢 ) |
16 |
15
|
unissd |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ∪ 𝑎 ⊆ ∪ 𝑢 ) |
17 |
|
sseq1 |
⊢ ( 𝑋 = ∪ 𝑎 → ( 𝑋 ⊆ ∪ 𝑢 ↔ ∪ 𝑎 ⊆ ∪ 𝑢 ) ) |
18 |
16 17
|
syl5ibrcom |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑋 = ∪ 𝑎 → 𝑋 ⊆ ∪ 𝑢 ) ) |
19 |
|
vex |
⊢ 𝑥 ∈ V |
20 |
|
inss1 |
⊢ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑥 |
21 |
19 20
|
elpwi2 |
⊢ ( 𝑥 ∩ 𝑢 ) ∈ 𝒫 𝑥 |
22 |
|
unieq |
⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → ∪ 𝑐 = ∪ ( 𝑥 ∩ 𝑢 ) ) |
23 |
22
|
eqeq2d |
⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → ( 𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
24 |
|
pweq |
⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → 𝒫 𝑐 = 𝒫 ( 𝑥 ∩ 𝑢 ) ) |
25 |
24
|
ineq1d |
⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → ( 𝒫 𝑐 ∩ Fin ) = ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) ) |
26 |
25
|
rexeqdv |
⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → ( ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ↔ ∃ 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) |
27 |
23 26
|
imbi12d |
⊢ ( 𝑐 = ( 𝑥 ∩ 𝑢 ) → ( ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ↔ ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) |
28 |
27
|
rspccv |
⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( ( 𝑥 ∩ 𝑢 ) ∈ 𝒫 𝑥 → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) ) |
29 |
21 28
|
mpi |
⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) |
30 |
|
inss2 |
⊢ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑢 |
31 |
|
sstr |
⊢ ( ( 𝑑 ⊆ ( 𝑥 ∩ 𝑢 ) ∧ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑢 ) → 𝑑 ⊆ 𝑢 ) |
32 |
30 31
|
mpan2 |
⊢ ( 𝑑 ⊆ ( 𝑥 ∩ 𝑢 ) → 𝑑 ⊆ 𝑢 ) |
33 |
32
|
anim1i |
⊢ ( ( 𝑑 ⊆ ( 𝑥 ∩ 𝑢 ) ∧ 𝑑 ∈ Fin ) → ( 𝑑 ⊆ 𝑢 ∧ 𝑑 ∈ Fin ) ) |
34 |
|
elfpw |
⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) ↔ ( 𝑑 ⊆ ( 𝑥 ∩ 𝑢 ) ∧ 𝑑 ∈ Fin ) ) |
35 |
|
elfpw |
⊢ ( 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) ↔ ( 𝑑 ⊆ 𝑢 ∧ 𝑑 ∈ Fin ) ) |
36 |
33 34 35
|
3imtr4i |
⊢ ( 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) → 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) ) |
37 |
36
|
anim1i |
⊢ ( ( 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) ∧ 𝑋 = ∪ 𝑑 ) → ( 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) ∧ 𝑋 = ∪ 𝑑 ) ) |
38 |
37
|
reximi2 |
⊢ ( ∃ 𝑑 ∈ ( 𝒫 ( 𝑥 ∩ 𝑢 ) ∩ Fin ) 𝑋 = ∪ 𝑑 → ∃ 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑑 ) |
39 |
29 38
|
syl6 |
⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) |
40 |
|
unieq |
⊢ ( 𝑑 = 𝑏 → ∪ 𝑑 = ∪ 𝑏 ) |
41 |
40
|
eqeq2d |
⊢ ( 𝑑 = 𝑏 → ( 𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ 𝑏 ) ) |
42 |
41
|
cbvrexvw |
⊢ ( ∃ 𝑑 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑑 ↔ ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ) |
43 |
39 42
|
syl6ib |
⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
44 |
|
dfrex2 |
⊢ ( ∃ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) 𝑋 = ∪ 𝑏 ↔ ¬ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) |
45 |
43 44
|
syl6ib |
⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) → ¬ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) |
46 |
45
|
con2d |
⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
47 |
46
|
a1d |
⊢ ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑎 ⊆ 𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) |
48 |
47
|
3ad2ant2 |
⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( 𝑎 ⊆ 𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) |
49 |
48
|
adantr |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( 𝑎 ⊆ 𝑢 → ( ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) |
50 |
49
|
impd |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
51 |
50
|
impr |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ¬ 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ) |
52 |
20
|
unissi |
⊢ ∪ ( 𝑥 ∩ 𝑢 ) ⊆ ∪ 𝑥 |
53 |
|
fiuni |
⊢ ( 𝑥 ∈ V → ∪ 𝑥 = ∪ ( fi ‘ 𝑥 ) ) |
54 |
53
|
elv |
⊢ ∪ 𝑥 = ∪ ( fi ‘ 𝑥 ) |
55 |
|
fibas |
⊢ ( fi ‘ 𝑥 ) ∈ TopBases |
56 |
|
unitg |
⊢ ( ( fi ‘ 𝑥 ) ∈ TopBases → ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) = ∪ ( fi ‘ 𝑥 ) ) |
57 |
55 56
|
ax-mp |
⊢ ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) = ∪ ( fi ‘ 𝑥 ) |
58 |
54 57
|
eqtr4i |
⊢ ∪ 𝑥 = ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) |
59 |
|
unieq |
⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ∪ 𝐽 = ∪ ( topGen ‘ ( fi ‘ 𝑥 ) ) ) |
60 |
58 59
|
eqtr4id |
⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ∪ 𝑥 = ∪ 𝐽 ) |
61 |
60 1
|
eqtr4di |
⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ∪ 𝑥 = 𝑋 ) |
62 |
61
|
3ad2ant1 |
⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ∪ 𝑥 = 𝑋 ) |
63 |
62
|
adantr |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ∪ 𝑥 = 𝑋 ) |
64 |
52 63
|
sseqtrid |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ∪ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑋 ) |
65 |
|
eqcom |
⊢ ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ↔ ∪ ( 𝑥 ∩ 𝑢 ) = 𝑋 ) |
66 |
|
eqss |
⊢ ( ∪ ( 𝑥 ∩ 𝑢 ) = 𝑋 ↔ ( ∪ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
67 |
66
|
baib |
⊢ ( ∪ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑋 → ( ∪ ( 𝑥 ∩ 𝑢 ) = 𝑋 ↔ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
68 |
65 67
|
syl5bb |
⊢ ( ∪ ( 𝑥 ∩ 𝑢 ) ⊆ 𝑋 → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ↔ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
69 |
64 68
|
syl |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑋 = ∪ ( 𝑥 ∩ 𝑢 ) ↔ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
70 |
51 69
|
mtbid |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ¬ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) |
71 |
|
sstr2 |
⊢ ( 𝑋 ⊆ ∪ 𝑢 → ( ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) → 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
72 |
71
|
con3rr3 |
⊢ ( ¬ 𝑋 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) → ( 𝑋 ⊆ ∪ 𝑢 → ¬ ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
73 |
70 72
|
syl |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑋 ⊆ ∪ 𝑢 → ¬ ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
74 |
|
nss |
⊢ ( ¬ ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ↔ ∃ 𝑦 ( 𝑦 ∈ ∪ 𝑢 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
75 |
|
df-rex |
⊢ ( ∃ 𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ↔ ∃ 𝑦 ( 𝑦 ∈ ∪ 𝑢 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
76 |
74 75
|
bitr4i |
⊢ ( ¬ ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) ↔ ∃ 𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) |
77 |
|
eluni2 |
⊢ ( 𝑦 ∈ ∪ 𝑢 ↔ ∃ 𝑤 ∈ 𝑢 𝑦 ∈ 𝑤 ) |
78 |
|
elpwi |
⊢ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) ) |
79 |
78
|
sseld |
⊢ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) → ( 𝑤 ∈ 𝑢 → 𝑤 ∈ ( fi ‘ 𝑥 ) ) ) |
80 |
79
|
ad2antrl |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑤 ∈ 𝑢 → 𝑤 ∈ ( fi ‘ 𝑥 ) ) ) |
81 |
|
elfi |
⊢ ( ( 𝑤 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑤 ∈ ( fi ‘ 𝑥 ) ↔ ∃ 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑤 = ∩ 𝑡 ) ) |
82 |
81
|
el2v |
⊢ ( 𝑤 ∈ ( fi ‘ 𝑥 ) ↔ ∃ 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑤 = ∩ 𝑡 ) |
83 |
80 82
|
syl6ib |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑤 ∈ 𝑢 → ∃ 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑤 = ∩ 𝑡 ) ) |
84 |
1
|
alexsubALTlem3 |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) → ∃ 𝑠 ∈ 𝑡 ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) |
85 |
78
|
adantr |
⊢ ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) ) |
86 |
85
|
ad4antlr |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑢 ⊆ ( fi ‘ 𝑥 ) ) |
87 |
|
ssfii |
⊢ ( 𝑥 ∈ V → 𝑥 ⊆ ( fi ‘ 𝑥 ) ) |
88 |
87
|
elv |
⊢ 𝑥 ⊆ ( fi ‘ 𝑥 ) |
89 |
|
elinel1 |
⊢ ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → 𝑡 ∈ 𝒫 𝑥 ) |
90 |
89
|
elpwid |
⊢ ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → 𝑡 ⊆ 𝑥 ) |
91 |
90
|
ad2antrr |
⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) → 𝑡 ⊆ 𝑥 ) |
92 |
91
|
ad2antlr |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑡 ⊆ 𝑥 ) |
93 |
|
simprl |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑠 ∈ 𝑡 ) |
94 |
92 93
|
sseldd |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑠 ∈ 𝑥 ) |
95 |
88 94
|
sselid |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑠 ∈ ( fi ‘ 𝑥 ) ) |
96 |
95
|
snssd |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → { 𝑠 } ⊆ ( fi ‘ 𝑥 ) ) |
97 |
86 96
|
unssd |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( 𝑢 ∪ { 𝑠 } ) ⊆ ( fi ‘ 𝑥 ) ) |
98 |
|
fvex |
⊢ ( fi ‘ 𝑥 ) ∈ V |
99 |
98
|
elpw2 |
⊢ ( ( 𝑢 ∪ { 𝑠 } ) ∈ 𝒫 ( fi ‘ 𝑥 ) ↔ ( 𝑢 ∪ { 𝑠 } ) ⊆ ( fi ‘ 𝑥 ) ) |
100 |
97 99
|
sylibr |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( 𝑢 ∪ { 𝑠 } ) ∈ 𝒫 ( fi ‘ 𝑥 ) ) |
101 |
|
simprl |
⊢ ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → 𝑎 ⊆ 𝑢 ) |
102 |
101
|
ad4antlr |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑎 ⊆ 𝑢 ) |
103 |
|
ssun1 |
⊢ 𝑢 ⊆ ( 𝑢 ∪ { 𝑠 } ) |
104 |
102 103
|
sstrdi |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑎 ⊆ ( 𝑢 ∪ { 𝑠 } ) ) |
105 |
|
unieq |
⊢ ( 𝑛 = 𝑏 → ∪ 𝑛 = ∪ 𝑏 ) |
106 |
105
|
eqeq2d |
⊢ ( 𝑛 = 𝑏 → ( 𝑋 = ∪ 𝑛 ↔ 𝑋 = ∪ 𝑏 ) ) |
107 |
106
|
notbid |
⊢ ( 𝑛 = 𝑏 → ( ¬ 𝑋 = ∪ 𝑛 ↔ ¬ 𝑋 = ∪ 𝑏 ) ) |
108 |
107
|
cbvralvw |
⊢ ( ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ↔ ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) |
109 |
108
|
biimpi |
⊢ ( ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 → ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) |
110 |
109
|
ad2antll |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) |
111 |
100 104 110
|
jca32 |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( ( 𝑢 ∪ { 𝑠 } ) ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ( 𝑢 ∪ { 𝑠 } ) ∧ ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
112 |
|
sseq2 |
⊢ ( 𝑧 = ( 𝑢 ∪ { 𝑠 } ) → ( 𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ ( 𝑢 ∪ { 𝑠 } ) ) ) |
113 |
|
pweq |
⊢ ( 𝑧 = ( 𝑢 ∪ { 𝑠 } ) → 𝒫 𝑧 = 𝒫 ( 𝑢 ∪ { 𝑠 } ) ) |
114 |
113
|
ineq1d |
⊢ ( 𝑧 = ( 𝑢 ∪ { 𝑠 } ) → ( 𝒫 𝑧 ∩ Fin ) = ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ) |
115 |
114
|
raleqdv |
⊢ ( 𝑧 = ( 𝑢 ∪ { 𝑠 } ) → ( ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) |
116 |
112 115
|
anbi12d |
⊢ ( 𝑧 = ( 𝑢 ∪ { 𝑠 } ) → ( ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ↔ ( 𝑎 ⊆ ( 𝑢 ∪ { 𝑠 } ) ∧ ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
117 |
116
|
elrab |
⊢ ( ( 𝑢 ∪ { 𝑠 } ) ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ↔ ( ( 𝑢 ∪ { 𝑠 } ) ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ( 𝑢 ∪ { 𝑠 } ) ∧ ∀ 𝑏 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
118 |
111 117
|
sylibr |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( 𝑢 ∪ { 𝑠 } ) ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) |
119 |
|
elun1 |
⊢ ( ( 𝑢 ∪ { 𝑠 } ) ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } → ( 𝑢 ∪ { 𝑠 } ) ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) |
120 |
118 119
|
syl |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( 𝑢 ∪ { 𝑠 } ) ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) |
121 |
|
vsnid |
⊢ 𝑠 ∈ { 𝑠 } |
122 |
|
elun2 |
⊢ ( 𝑠 ∈ { 𝑠 } → 𝑠 ∈ ( 𝑢 ∪ { 𝑠 } ) ) |
123 |
121 122
|
ax-mp |
⊢ 𝑠 ∈ ( 𝑢 ∪ { 𝑠 } ) |
124 |
|
intss1 |
⊢ ( 𝑠 ∈ 𝑡 → ∩ 𝑡 ⊆ 𝑠 ) |
125 |
|
sseq1 |
⊢ ( 𝑤 = ∩ 𝑡 → ( 𝑤 ⊆ 𝑠 ↔ ∩ 𝑡 ⊆ 𝑠 ) ) |
126 |
124 125
|
syl5ibrcom |
⊢ ( 𝑠 ∈ 𝑡 → ( 𝑤 = ∩ 𝑡 → 𝑤 ⊆ 𝑠 ) ) |
127 |
126
|
impcom |
⊢ ( ( 𝑤 = ∩ 𝑡 ∧ 𝑠 ∈ 𝑡 ) → 𝑤 ⊆ 𝑠 ) |
128 |
127
|
ad4ant24 |
⊢ ( ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ 𝑠 ∈ 𝑡 ) → 𝑤 ⊆ 𝑠 ) |
129 |
128
|
adantl |
⊢ ( ( 𝑤 ∈ 𝑢 ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ 𝑠 ∈ 𝑡 ) ) → 𝑤 ⊆ 𝑠 ) |
130 |
129
|
adantrrr |
⊢ ( ( 𝑤 ∈ 𝑢 ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑤 ⊆ 𝑠 ) |
131 |
130
|
adantll |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑤 ⊆ 𝑠 ) |
132 |
|
simprlr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑦 ∈ 𝑤 ) |
133 |
131 132
|
sseldd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑦 ∈ 𝑠 ) |
134 |
90
|
ad2antrr |
⊢ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) → 𝑡 ⊆ 𝑥 ) |
135 |
134
|
ad2antrl |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑡 ⊆ 𝑥 ) |
136 |
|
simprrl |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑠 ∈ 𝑡 ) |
137 |
135 136
|
sseldd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → 𝑠 ∈ 𝑥 ) |
138 |
|
elin |
⊢ ( 𝑠 ∈ ( 𝑥 ∩ 𝑢 ) ↔ ( 𝑠 ∈ 𝑥 ∧ 𝑠 ∈ 𝑢 ) ) |
139 |
|
elunii |
⊢ ( ( 𝑦 ∈ 𝑠 ∧ 𝑠 ∈ ( 𝑥 ∩ 𝑢 ) ) → 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) |
140 |
139
|
ex |
⊢ ( 𝑦 ∈ 𝑠 → ( 𝑠 ∈ ( 𝑥 ∩ 𝑢 ) → 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
141 |
138 140
|
syl5bir |
⊢ ( 𝑦 ∈ 𝑠 → ( ( 𝑠 ∈ 𝑥 ∧ 𝑠 ∈ 𝑢 ) → 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
142 |
141
|
expd |
⊢ ( 𝑦 ∈ 𝑠 → ( 𝑠 ∈ 𝑥 → ( 𝑠 ∈ 𝑢 → 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) |
143 |
133 137 142
|
sylc |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → ( 𝑠 ∈ 𝑢 → 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) |
144 |
143
|
con3d |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) ) → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ¬ 𝑠 ∈ 𝑢 ) ) |
145 |
144
|
expr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ) → ( ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ¬ 𝑠 ∈ 𝑢 ) ) ) |
146 |
145
|
com23 |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ 𝑦 ∈ 𝑤 ) ) → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ( ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) → ¬ 𝑠 ∈ 𝑢 ) ) ) |
147 |
146
|
exp32 |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ( ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) → ¬ 𝑠 ∈ 𝑢 ) ) ) ) ) |
148 |
147
|
imp55 |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ¬ 𝑠 ∈ 𝑢 ) |
149 |
|
vex |
⊢ 𝑠 ∈ V |
150 |
|
eleq1w |
⊢ ( 𝑣 = 𝑠 → ( 𝑣 ∈ ( 𝑢 ∪ { 𝑠 } ) ↔ 𝑠 ∈ ( 𝑢 ∪ { 𝑠 } ) ) ) |
151 |
|
elequ1 |
⊢ ( 𝑣 = 𝑠 → ( 𝑣 ∈ 𝑢 ↔ 𝑠 ∈ 𝑢 ) ) |
152 |
151
|
notbid |
⊢ ( 𝑣 = 𝑠 → ( ¬ 𝑣 ∈ 𝑢 ↔ ¬ 𝑠 ∈ 𝑢 ) ) |
153 |
150 152
|
anbi12d |
⊢ ( 𝑣 = 𝑠 → ( ( 𝑣 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑣 ∈ 𝑢 ) ↔ ( 𝑠 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑠 ∈ 𝑢 ) ) ) |
154 |
149 153
|
spcev |
⊢ ( ( 𝑠 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑠 ∈ 𝑢 ) → ∃ 𝑣 ( 𝑣 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑣 ∈ 𝑢 ) ) |
155 |
123 148 154
|
sylancr |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ∃ 𝑣 ( 𝑣 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑣 ∈ 𝑢 ) ) |
156 |
|
nss |
⊢ ( ¬ ( 𝑢 ∪ { 𝑠 } ) ⊆ 𝑢 ↔ ∃ 𝑣 ( 𝑣 ∈ ( 𝑢 ∪ { 𝑠 } ) ∧ ¬ 𝑣 ∈ 𝑢 ) ) |
157 |
155 156
|
sylibr |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ¬ ( 𝑢 ∪ { 𝑠 } ) ⊆ 𝑢 ) |
158 |
|
eqimss2 |
⊢ ( 𝑢 = ( 𝑢 ∪ { 𝑠 } ) → ( 𝑢 ∪ { 𝑠 } ) ⊆ 𝑢 ) |
159 |
158
|
necon3bi |
⊢ ( ¬ ( 𝑢 ∪ { 𝑠 } ) ⊆ 𝑢 → 𝑢 ≠ ( 𝑢 ∪ { 𝑠 } ) ) |
160 |
157 159
|
syl |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑢 ≠ ( 𝑢 ∪ { 𝑠 } ) ) |
161 |
160 103
|
jctil |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ( 𝑢 ⊆ ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑢 ≠ ( 𝑢 ∪ { 𝑠 } ) ) ) |
162 |
|
df-pss |
⊢ ( 𝑢 ⊊ ( 𝑢 ∪ { 𝑠 } ) ↔ ( 𝑢 ⊆ ( 𝑢 ∪ { 𝑠 } ) ∧ 𝑢 ≠ ( 𝑢 ∪ { 𝑠 } ) ) ) |
163 |
161 162
|
sylibr |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → 𝑢 ⊊ ( 𝑢 ∪ { 𝑠 } ) ) |
164 |
|
psseq2 |
⊢ ( 𝑣 = ( 𝑢 ∪ { 𝑠 } ) → ( 𝑢 ⊊ 𝑣 ↔ 𝑢 ⊊ ( 𝑢 ∪ { 𝑠 } ) ) ) |
165 |
164
|
rspcev |
⊢ ( ( ( 𝑢 ∪ { 𝑠 } ) ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ 𝑢 ⊊ ( 𝑢 ∪ { 𝑠 } ) ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) |
166 |
120 163 165
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) ∧ ( 𝑠 ∈ 𝑡 ∧ ∀ 𝑛 ∈ ( 𝒫 ( 𝑢 ∪ { 𝑠 } ) ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) |
167 |
84 166
|
rexlimddv |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) ∧ ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) ) ) ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) |
168 |
167
|
exp45 |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) ∧ 𝑤 = ∩ 𝑡 ) → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) ) |
169 |
168
|
expd |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) → ( 𝑤 = ∩ 𝑡 → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) ) ) |
170 |
169
|
rexlimdv |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ∧ 𝑤 ∈ 𝑢 ) → ( ∃ 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑤 = ∩ 𝑡 → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) ) |
171 |
170
|
ex |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑤 ∈ 𝑢 → ( ∃ 𝑡 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑤 = ∩ 𝑡 → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) ) ) |
172 |
83 171
|
mpdd |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑤 ∈ 𝑢 → ( 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) ) |
173 |
172
|
rexlimdv |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( ∃ 𝑤 ∈ 𝑢 𝑦 ∈ 𝑤 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) |
174 |
77 173
|
syl5bi |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑦 ∈ ∪ 𝑢 → ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) ) |
175 |
174
|
rexlimdv |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( ∃ 𝑦 ∈ ∪ 𝑢 ¬ 𝑦 ∈ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) |
176 |
76 175
|
syl5bi |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( ¬ ∪ 𝑢 ⊆ ∪ ( 𝑥 ∩ 𝑢 ) → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) |
177 |
18 73 176
|
3syld |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( 𝑋 = ∪ 𝑎 → ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 ) ) |
178 |
177
|
con3d |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( ¬ ∃ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) |
179 |
14 178
|
syl5bi |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) |
180 |
179
|
ex |
⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) ) |
181 |
180
|
adantr |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) ) |
182 |
|
ssun1 |
⊢ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) |
183 |
|
eqimss2 |
⊢ ( 𝑧 = 𝑎 → 𝑎 ⊆ 𝑧 ) |
184 |
183
|
biantrurd |
⊢ ( 𝑧 = 𝑎 → ( ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
185 |
|
pweq |
⊢ ( 𝑧 = 𝑎 → 𝒫 𝑧 = 𝒫 𝑎 ) |
186 |
185
|
ineq1d |
⊢ ( 𝑧 = 𝑎 → ( 𝒫 𝑧 ∩ Fin ) = ( 𝒫 𝑎 ∩ Fin ) ) |
187 |
186
|
raleqdv |
⊢ ( 𝑧 = 𝑎 → ( ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) |
188 |
184 187
|
bitr3d |
⊢ ( 𝑧 = 𝑎 → ( ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) |
189 |
|
simpll3 |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) |
190 |
|
simplr |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) |
191 |
188 189 190
|
elrabd |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → 𝑎 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) |
192 |
182 191
|
sselid |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → 𝑎 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) |
193 |
|
psseq2 |
⊢ ( 𝑣 = 𝑎 → ( 𝑢 ⊊ 𝑣 ↔ 𝑢 ⊊ 𝑎 ) ) |
194 |
193
|
notbid |
⊢ ( 𝑣 = 𝑎 → ( ¬ 𝑢 ⊊ 𝑣 ↔ ¬ 𝑢 ⊊ 𝑎 ) ) |
195 |
194
|
rspcv |
⊢ ( 𝑎 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑢 ⊊ 𝑎 ) ) |
196 |
192 195
|
syl |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑢 ⊊ 𝑎 ) ) |
197 |
|
id |
⊢ ( 𝑎 = ∅ → 𝑎 = ∅ ) |
198 |
|
0elpw |
⊢ ∅ ∈ 𝒫 𝑎 |
199 |
|
0fin |
⊢ ∅ ∈ Fin |
200 |
198 199
|
elini |
⊢ ∅ ∈ ( 𝒫 𝑎 ∩ Fin ) |
201 |
197 200
|
eqeltrdi |
⊢ ( 𝑎 = ∅ → 𝑎 ∈ ( 𝒫 𝑎 ∩ Fin ) ) |
202 |
|
unieq |
⊢ ( 𝑏 = 𝑎 → ∪ 𝑏 = ∪ 𝑎 ) |
203 |
202
|
eqeq2d |
⊢ ( 𝑏 = 𝑎 → ( 𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ 𝑎 ) ) |
204 |
203
|
notbid |
⊢ ( 𝑏 = 𝑎 → ( ¬ 𝑋 = ∪ 𝑏 ↔ ¬ 𝑋 = ∪ 𝑎 ) ) |
205 |
204
|
rspccv |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑎 ∈ ( 𝒫 𝑎 ∩ Fin ) → ¬ 𝑋 = ∪ 𝑎 ) ) |
206 |
201 205
|
syl5 |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑎 = ∅ → ¬ 𝑋 = ∪ 𝑎 ) ) |
207 |
206
|
necon2ad |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑋 = ∪ 𝑎 → 𝑎 ≠ ∅ ) ) |
208 |
207
|
ad2antlr |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( 𝑋 = ∪ 𝑎 → 𝑎 ≠ ∅ ) ) |
209 |
|
psseq1 |
⊢ ( 𝑢 = ∅ → ( 𝑢 ⊊ 𝑎 ↔ ∅ ⊊ 𝑎 ) ) |
210 |
209
|
adantl |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( 𝑢 ⊊ 𝑎 ↔ ∅ ⊊ 𝑎 ) ) |
211 |
|
0pss |
⊢ ( ∅ ⊊ 𝑎 ↔ 𝑎 ≠ ∅ ) |
212 |
210 211
|
bitrdi |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( 𝑢 ⊊ 𝑎 ↔ 𝑎 ≠ ∅ ) ) |
213 |
208 212
|
sylibrd |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( 𝑋 = ∪ 𝑎 → 𝑢 ⊊ 𝑎 ) ) |
214 |
196 213
|
nsyld |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ 𝑢 = ∅ ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) |
215 |
214
|
ex |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( 𝑢 = ∅ → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) ) |
216 |
181 215
|
jaod |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( ( ( 𝑢 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑢 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑢 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ∨ 𝑢 = ∅ ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) ) |
217 |
13 216
|
syl5bi |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ( ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) ) |
218 |
217
|
rexlimdv |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( ∃ 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 → ¬ 𝑋 = ∪ 𝑎 ) ) |
219 |
3 218
|
mpd |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ¬ 𝑋 = ∪ 𝑎 ) |
220 |
219
|
ex |
⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ 𝑎 ) ) |
221 |
2 220
|
syl5bir |
⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( ¬ ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ 𝑎 ) ) |
222 |
221
|
con4d |
⊢ ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) → ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
223 |
222
|
3exp |
⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ( 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) → ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) ) |
224 |
223
|
ralrimdv |
⊢ ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) → ∀ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |