Step |
Hyp |
Ref |
Expression |
1 |
|
comppfsc.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
elpwi |
⊢ ( 𝑐 ∈ 𝒫 𝐽 → 𝑐 ⊆ 𝐽 ) |
3 |
1
|
cmpcov |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) |
4 |
|
elfpw |
⊢ ( 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) ↔ ( 𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin ) ) |
5 |
|
finptfin |
⊢ ( 𝑑 ∈ Fin → 𝑑 ∈ PtFin ) |
6 |
5
|
anim1i |
⊢ ( ( 𝑑 ∈ Fin ∧ ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ PtFin ∧ ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) |
7 |
6
|
anassrs |
⊢ ( ( ( 𝑑 ∈ Fin ∧ 𝑑 ⊆ 𝑐 ) ∧ 𝑋 = ∪ 𝑑 ) → ( 𝑑 ∈ PtFin ∧ ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) |
8 |
7
|
ancom1s |
⊢ ( ( ( 𝑑 ⊆ 𝑐 ∧ 𝑑 ∈ Fin ) ∧ 𝑋 = ∪ 𝑑 ) → ( 𝑑 ∈ PtFin ∧ ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) |
9 |
4 8
|
sylanb |
⊢ ( ( 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑋 = ∪ 𝑑 ) → ( 𝑑 ∈ PtFin ∧ ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) |
10 |
9
|
reximi2 |
⊢ ( ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) |
11 |
3 10
|
syl |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) |
12 |
11
|
3exp |
⊢ ( 𝐽 ∈ Comp → ( 𝑐 ⊆ 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) ) |
13 |
2 12
|
syl5 |
⊢ ( 𝐽 ∈ Comp → ( 𝑐 ∈ 𝒫 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) ) |
14 |
13
|
ralrimiv |
⊢ ( 𝐽 ∈ Comp → ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) |
15 |
|
elpwi |
⊢ ( 𝑎 ∈ 𝒫 𝐽 → 𝑎 ⊆ 𝐽 ) |
16 |
|
0elpw |
⊢ ∅ ∈ 𝒫 𝑎 |
17 |
|
0fin |
⊢ ∅ ∈ Fin |
18 |
16 17
|
elini |
⊢ ∅ ∈ ( 𝒫 𝑎 ∩ Fin ) |
19 |
|
unieq |
⊢ ( 𝑏 = ∅ → ∪ 𝑏 = ∪ ∅ ) |
20 |
|
uni0 |
⊢ ∪ ∅ = ∅ |
21 |
19 20
|
eqtrdi |
⊢ ( 𝑏 = ∅ → ∪ 𝑏 = ∅ ) |
22 |
21
|
rspceeqv |
⊢ ( ( ∅ ∈ ( 𝒫 𝑎 ∩ Fin ) ∧ 𝑋 = ∅ ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) |
23 |
18 22
|
mpan |
⊢ ( 𝑋 = ∅ → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) |
24 |
23
|
a1i13 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑋 = ∅ → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |
25 |
|
n0 |
⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑋 ) |
26 |
|
simp2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → 𝑋 = ∪ 𝑎 ) |
27 |
26
|
eleq2d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ∪ 𝑎 ) ) |
28 |
27
|
biimpd |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑥 ∈ 𝑋 → 𝑥 ∈ ∪ 𝑎 ) ) |
29 |
|
eluni2 |
⊢ ( 𝑥 ∈ ∪ 𝑎 ↔ ∃ 𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 ) |
30 |
28 29
|
syl6ib |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑥 ∈ 𝑋 → ∃ 𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 ) ) |
31 |
|
simpl3 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑎 ⊆ 𝐽 ) |
32 |
|
simprl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑠 ∈ 𝑎 ) |
33 |
31 32
|
sseldd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑠 ∈ 𝐽 ) |
34 |
|
elssuni |
⊢ ( 𝑠 ∈ 𝐽 → 𝑠 ⊆ ∪ 𝐽 ) |
35 |
34 1
|
sseqtrrdi |
⊢ ( 𝑠 ∈ 𝐽 → 𝑠 ⊆ 𝑋 ) |
36 |
33 35
|
syl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑠 ⊆ 𝑋 ) |
37 |
36
|
ralrimivw |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ∀ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ) |
38 |
|
iunss |
⊢ ( ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ ∀ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ) |
39 |
37 38
|
sylibr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ) |
40 |
|
ssequn1 |
⊢ ( ∪ 𝑝 ∈ 𝑎 𝑠 ⊆ 𝑋 ↔ ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋 ) = 𝑋 ) |
41 |
39 40
|
sylib |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋 ) = 𝑋 ) |
42 |
|
simpl2 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑋 = ∪ 𝑎 ) |
43 |
|
uniiun |
⊢ ∪ 𝑎 = ∪ 𝑝 ∈ 𝑎 𝑝 |
44 |
42 43
|
eqtrdi |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑋 = ∪ 𝑝 ∈ 𝑎 𝑝 ) |
45 |
44
|
uneq2d |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ 𝑋 ) = ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝 ) ) |
46 |
41 45
|
eqtr3d |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑋 = ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝 ) ) |
47 |
|
iunun |
⊢ ∪ 𝑝 ∈ 𝑎 ( 𝑠 ∪ 𝑝 ) = ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝 ) |
48 |
|
vex |
⊢ 𝑠 ∈ V |
49 |
|
vex |
⊢ 𝑝 ∈ V |
50 |
48 49
|
unex |
⊢ ( 𝑠 ∪ 𝑝 ) ∈ V |
51 |
50
|
dfiun3 |
⊢ ∪ 𝑝 ∈ 𝑎 ( 𝑠 ∪ 𝑝 ) = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) |
52 |
47 51
|
eqtr3i |
⊢ ( ∪ 𝑝 ∈ 𝑎 𝑠 ∪ ∪ 𝑝 ∈ 𝑎 𝑝 ) = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) |
53 |
46 52
|
eqtrdi |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑋 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ) |
54 |
|
simpll1 |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ 𝑝 ∈ 𝑎 ) → 𝐽 ∈ Top ) |
55 |
33
|
adantr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ 𝑝 ∈ 𝑎 ) → 𝑠 ∈ 𝐽 ) |
56 |
31
|
sselda |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ 𝑝 ∈ 𝑎 ) → 𝑝 ∈ 𝐽 ) |
57 |
|
unopn |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑠 ∈ 𝐽 ∧ 𝑝 ∈ 𝐽 ) → ( 𝑠 ∪ 𝑝 ) ∈ 𝐽 ) |
58 |
54 55 56 57
|
syl3anc |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ 𝑝 ∈ 𝑎 ) → ( 𝑠 ∪ 𝑝 ) ∈ 𝐽 ) |
59 |
58
|
fmpttd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) : 𝑎 ⟶ 𝐽 ) |
60 |
59
|
frnd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ⊆ 𝐽 ) |
61 |
|
elpw2g |
⊢ ( 𝐽 ∈ Top → ( ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∈ 𝒫 𝐽 ↔ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ⊆ 𝐽 ) ) |
62 |
61
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∈ 𝒫 𝐽 ↔ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ⊆ 𝐽 ) ) |
63 |
62
|
adantr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∈ 𝒫 𝐽 ↔ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ⊆ 𝐽 ) ) |
64 |
60 63
|
mpbird |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∈ 𝒫 𝐽 ) |
65 |
|
unieq |
⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ∪ 𝑐 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ) |
66 |
65
|
eqeq2d |
⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( 𝑋 = ∪ 𝑐 ↔ 𝑋 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ) ) |
67 |
|
sseq2 |
⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( 𝑑 ⊆ 𝑐 ↔ 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ) ) |
68 |
67
|
anbi1d |
⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ↔ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ) |
69 |
68
|
rexbidv |
⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ↔ ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ) |
70 |
66 69
|
imbi12d |
⊢ ( 𝑐 = ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ↔ ( 𝑋 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ) ) |
71 |
70
|
rspcv |
⊢ ( ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∈ 𝒫 𝐽 → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑋 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ) ) |
72 |
64 71
|
syl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑋 = ∪ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ) ) |
73 |
53 72
|
mpid |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ) |
74 |
|
simprr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑥 ∈ 𝑠 ) |
75 |
|
ssel2 |
⊢ ( ( 𝑎 ⊆ 𝐽 ∧ 𝑠 ∈ 𝑎 ) → 𝑠 ∈ 𝐽 ) |
76 |
75
|
3ad2antl3 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ 𝑠 ∈ 𝑎 ) → 𝑠 ∈ 𝐽 ) |
77 |
76
|
adantrr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑠 ∈ 𝐽 ) |
78 |
|
elunii |
⊢ ( ( 𝑥 ∈ 𝑠 ∧ 𝑠 ∈ 𝐽 ) → 𝑥 ∈ ∪ 𝐽 ) |
79 |
74 77 78
|
syl2anc |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑥 ∈ ∪ 𝐽 ) |
80 |
79 1
|
eleqtrrdi |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑥 ∈ 𝑋 ) |
81 |
80
|
adantr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑥 ∈ 𝑋 ) |
82 |
|
simprr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑋 = ∪ 𝑑 ) |
83 |
81 82
|
eleqtrd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑥 ∈ ∪ 𝑑 ) |
84 |
|
eqid |
⊢ ∪ 𝑑 = ∪ 𝑑 |
85 |
84
|
ptfinfin |
⊢ ( ( 𝑑 ∈ PtFin ∧ 𝑥 ∈ ∪ 𝑑 ) → { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ∈ Fin ) |
86 |
85
|
expcom |
⊢ ( 𝑥 ∈ ∪ 𝑑 → ( 𝑑 ∈ PtFin → { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ∈ Fin ) ) |
87 |
83 86
|
syl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ PtFin → { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ∈ Fin ) ) |
88 |
|
simprl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ) |
89 |
|
elun1 |
⊢ ( 𝑥 ∈ 𝑠 → 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) ) |
90 |
89
|
ad2antll |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) ) |
91 |
90
|
ralrimivw |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ∀ 𝑝 ∈ 𝑎 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) ) |
92 |
50
|
rgenw |
⊢ ∀ 𝑝 ∈ 𝑎 ( 𝑠 ∪ 𝑝 ) ∈ V |
93 |
|
eqid |
⊢ ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) = ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) |
94 |
|
eleq2 |
⊢ ( 𝑧 = ( 𝑠 ∪ 𝑝 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) ) ) |
95 |
93 94
|
ralrnmptw |
⊢ ( ∀ 𝑝 ∈ 𝑎 ( 𝑠 ∪ 𝑝 ) ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) 𝑥 ∈ 𝑧 ↔ ∀ 𝑝 ∈ 𝑎 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) ) ) |
96 |
92 95
|
ax-mp |
⊢ ( ∀ 𝑧 ∈ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) 𝑥 ∈ 𝑧 ↔ ∀ 𝑝 ∈ 𝑎 𝑥 ∈ ( 𝑠 ∪ 𝑝 ) ) |
97 |
91 96
|
sylibr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ∀ 𝑧 ∈ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) 𝑥 ∈ 𝑧 ) |
98 |
97
|
adantr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ∀ 𝑧 ∈ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) 𝑥 ∈ 𝑧 ) |
99 |
|
ssralv |
⊢ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) → ( ∀ 𝑧 ∈ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) 𝑥 ∈ 𝑧 → ∀ 𝑧 ∈ 𝑑 𝑥 ∈ 𝑧 ) ) |
100 |
88 98 99
|
sylc |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ∀ 𝑧 ∈ 𝑑 𝑥 ∈ 𝑧 ) |
101 |
|
rabid2 |
⊢ ( 𝑑 = { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ↔ ∀ 𝑧 ∈ 𝑑 𝑥 ∈ 𝑧 ) |
102 |
100 101
|
sylibr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑑 = { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ) |
103 |
102
|
eleq1d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ Fin ↔ { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ∈ Fin ) ) |
104 |
103
|
biimprd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( { 𝑧 ∈ 𝑑 ∣ 𝑥 ∈ 𝑧 } ∈ Fin → 𝑑 ∈ Fin ) ) |
105 |
93
|
rnmpt |
⊢ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) = { 𝑞 ∣ ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) } |
106 |
88 105
|
sseqtrdi |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → 𝑑 ⊆ { 𝑞 ∣ ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) } ) |
107 |
|
ssabral |
⊢ ( 𝑑 ⊆ { 𝑞 ∣ ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) } ↔ ∀ 𝑞 ∈ 𝑑 ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) ) |
108 |
106 107
|
sylib |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ∀ 𝑞 ∈ 𝑑 ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) ) |
109 |
|
uneq2 |
⊢ ( 𝑝 = ( 𝑓 ‘ 𝑞 ) → ( 𝑠 ∪ 𝑝 ) = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) |
110 |
109
|
eqeq2d |
⊢ ( 𝑝 = ( 𝑓 ‘ 𝑞 ) → ( 𝑞 = ( 𝑠 ∪ 𝑝 ) ↔ 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) |
111 |
110
|
ac6sfi |
⊢ ( ( 𝑑 ∈ Fin ∧ ∀ 𝑞 ∈ 𝑑 ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) ) → ∃ 𝑓 ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) |
112 |
111
|
expcom |
⊢ ( ∀ 𝑞 ∈ 𝑑 ∃ 𝑝 ∈ 𝑎 𝑞 = ( 𝑠 ∪ 𝑝 ) → ( 𝑑 ∈ Fin → ∃ 𝑓 ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) |
113 |
108 112
|
syl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ Fin → ∃ 𝑓 ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) |
114 |
|
frn |
⊢ ( 𝑓 : 𝑑 ⟶ 𝑎 → ran 𝑓 ⊆ 𝑎 ) |
115 |
114
|
adantr |
⊢ ( ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) → ran 𝑓 ⊆ 𝑎 ) |
116 |
115
|
ad2antll |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ran 𝑓 ⊆ 𝑎 ) |
117 |
32
|
ad2antrr |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑠 ∈ 𝑎 ) |
118 |
117
|
snssd |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → { 𝑠 } ⊆ 𝑎 ) |
119 |
116 118
|
unssd |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝑎 ) |
120 |
|
simprl |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑑 ∈ Fin ) |
121 |
|
simprrl |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑓 : 𝑑 ⟶ 𝑎 ) |
122 |
121
|
ffnd |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑓 Fn 𝑑 ) |
123 |
|
dffn4 |
⊢ ( 𝑓 Fn 𝑑 ↔ 𝑓 : 𝑑 –onto→ ran 𝑓 ) |
124 |
122 123
|
sylib |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑓 : 𝑑 –onto→ ran 𝑓 ) |
125 |
|
fofi |
⊢ ( ( 𝑑 ∈ Fin ∧ 𝑓 : 𝑑 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin ) |
126 |
120 124 125
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ran 𝑓 ∈ Fin ) |
127 |
|
snfi |
⊢ { 𝑠 } ∈ Fin |
128 |
|
unfi |
⊢ ( ( ran 𝑓 ∈ Fin ∧ { 𝑠 } ∈ Fin ) → ( ran 𝑓 ∪ { 𝑠 } ) ∈ Fin ) |
129 |
126 127 128
|
sylancl |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ( ran 𝑓 ∪ { 𝑠 } ) ∈ Fin ) |
130 |
|
elfpw |
⊢ ( ( ran 𝑓 ∪ { 𝑠 } ) ∈ ( 𝒫 𝑎 ∩ Fin ) ↔ ( ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝑎 ∧ ( ran 𝑓 ∪ { 𝑠 } ) ∈ Fin ) ) |
131 |
119 129 130
|
sylanbrc |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ( ran 𝑓 ∪ { 𝑠 } ) ∈ ( 𝒫 𝑎 ∩ Fin ) ) |
132 |
|
simplrr |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑋 = ∪ 𝑑 ) |
133 |
|
uniiun |
⊢ ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 𝑞 |
134 |
|
simprrr |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) |
135 |
|
iuneq2 |
⊢ ( ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) |
136 |
134 135
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ∪ 𝑞 ∈ 𝑑 𝑞 = ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) |
137 |
133 136
|
syl5eq |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ∪ 𝑑 = ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) |
138 |
132 137
|
eqtrd |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑋 = ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) |
139 |
|
ssun2 |
⊢ { 𝑠 } ⊆ ( ran 𝑓 ∪ { 𝑠 } ) |
140 |
|
vsnid |
⊢ 𝑠 ∈ { 𝑠 } |
141 |
139 140
|
sselii |
⊢ 𝑠 ∈ ( ran 𝑓 ∪ { 𝑠 } ) |
142 |
|
elssuni |
⊢ ( 𝑠 ∈ ( ran 𝑓 ∪ { 𝑠 } ) → 𝑠 ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) ) |
143 |
141 142
|
ax-mp |
⊢ 𝑠 ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) |
144 |
|
fvssunirn |
⊢ ( 𝑓 ‘ 𝑞 ) ⊆ ∪ ran 𝑓 |
145 |
|
ssun1 |
⊢ ran 𝑓 ⊆ ( ran 𝑓 ∪ { 𝑠 } ) |
146 |
145
|
unissi |
⊢ ∪ ran 𝑓 ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) |
147 |
144 146
|
sstri |
⊢ ( 𝑓 ‘ 𝑞 ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) |
148 |
143 147
|
unssi |
⊢ ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) |
149 |
148
|
rgenw |
⊢ ∀ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) |
150 |
|
iunss |
⊢ ( ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) ↔ ∀ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) ) |
151 |
149 150
|
mpbir |
⊢ ∪ 𝑞 ∈ 𝑑 ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) |
152 |
138 151
|
eqsstrdi |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑋 ⊆ ∪ ( ran 𝑓 ∪ { 𝑠 } ) ) |
153 |
31
|
ad2antrr |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑎 ⊆ 𝐽 ) |
154 |
116 153
|
sstrd |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ran 𝑓 ⊆ 𝐽 ) |
155 |
33
|
ad2antrr |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑠 ∈ 𝐽 ) |
156 |
155
|
snssd |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → { 𝑠 } ⊆ 𝐽 ) |
157 |
154 156
|
unssd |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝐽 ) |
158 |
|
uniss |
⊢ ( ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝐽 → ∪ ( ran 𝑓 ∪ { 𝑠 } ) ⊆ ∪ 𝐽 ) |
159 |
158 1
|
sseqtrrdi |
⊢ ( ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝐽 → ∪ ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝑋 ) |
160 |
157 159
|
syl |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ∪ ( ran 𝑓 ∪ { 𝑠 } ) ⊆ 𝑋 ) |
161 |
152 160
|
eqssd |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → 𝑋 = ∪ ( ran 𝑓 ∪ { 𝑠 } ) ) |
162 |
|
unieq |
⊢ ( 𝑏 = ( ran 𝑓 ∪ { 𝑠 } ) → ∪ 𝑏 = ∪ ( ran 𝑓 ∪ { 𝑠 } ) ) |
163 |
162
|
rspceeqv |
⊢ ( ( ( ran 𝑓 ∪ { 𝑠 } ) ∈ ( 𝒫 𝑎 ∩ Fin ) ∧ 𝑋 = ∪ ( ran 𝑓 ∪ { 𝑠 } ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) |
164 |
131 161 163
|
syl2anc |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ ( 𝑑 ∈ Fin ∧ ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) |
165 |
164
|
expr |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ 𝑑 ∈ Fin ) → ( ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
166 |
165
|
exlimdv |
⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) ∧ 𝑑 ∈ Fin ) → ( ∃ 𝑓 ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
167 |
166
|
ex |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ Fin → ( ∃ 𝑓 ( 𝑓 : 𝑑 ⟶ 𝑎 ∧ ∀ 𝑞 ∈ 𝑑 𝑞 = ( 𝑠 ∪ ( 𝑓 ‘ 𝑞 ) ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |
168 |
113 167
|
mpdd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ Fin → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
169 |
87 104 168
|
3syld |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) ∧ ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑑 ∈ PtFin → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
170 |
169
|
ex |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) → ( 𝑑 ∈ PtFin → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |
171 |
170
|
com23 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( 𝑑 ∈ PtFin → ( ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |
172 |
171
|
rexlimdv |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ ran ( 𝑝 ∈ 𝑎 ↦ ( 𝑠 ∪ 𝑝 ) ) ∧ 𝑋 = ∪ 𝑑 ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
173 |
73 172
|
syld |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) ∧ ( 𝑠 ∈ 𝑎 ∧ 𝑥 ∈ 𝑠 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
174 |
173
|
rexlimdvaa |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( ∃ 𝑠 ∈ 𝑎 𝑥 ∈ 𝑠 → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |
175 |
30 174
|
syld |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑥 ∈ 𝑋 → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |
176 |
175
|
exlimdv |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( ∃ 𝑥 𝑥 ∈ 𝑋 → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |
177 |
25 176
|
syl5bi |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( 𝑋 ≠ ∅ → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |
178 |
24 177
|
pm2.61dne |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ⊆ 𝐽 ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
179 |
15 178
|
syl3an3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 = ∪ 𝑎 ∧ 𝑎 ∈ 𝒫 𝐽 ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) |
180 |
179
|
3exp |
⊢ ( 𝐽 ∈ Top → ( 𝑋 = ∪ 𝑎 → ( 𝑎 ∈ 𝒫 𝐽 → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) ) |
181 |
180
|
com24 |
⊢ ( 𝐽 ∈ Top → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ( 𝑎 ∈ 𝒫 𝐽 → ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) ) |
182 |
181
|
ralrimdv |
⊢ ( 𝐽 ∈ Top → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → ∀ 𝑎 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |
183 |
1
|
iscmp |
⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑎 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ) ) |
184 |
183
|
baibr |
⊢ ( 𝐽 ∈ Top → ( ∀ 𝑎 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑎 → ∃ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) 𝑋 = ∪ 𝑏 ) ↔ 𝐽 ∈ Comp ) ) |
185 |
182 184
|
sylibd |
⊢ ( 𝐽 ∈ Top → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) → 𝐽 ∈ Comp ) ) |
186 |
14 185
|
impbid2 |
⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Comp ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ PtFin ( 𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑 ) ) ) ) |