Step | Hyp | Ref
| Expression |
1 | | simprr 796 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) → (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢) |
2 | | ssun2 3777 |
. . . . . . . . 9
⊢ {𝐴} ⊆ (ran 𝐹 ∪ {𝐴}) |
3 | | 1stckgen.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
4 | | 1stckgen.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝐴) |
5 | | lmcl 21101 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝐴) → 𝐴 ∈ 𝑋) |
6 | 3, 4, 5 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
7 | | snssg 4327 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑋 → (𝐴 ∈ (ran 𝐹 ∪ {𝐴}) ↔ {𝐴} ⊆ (ran 𝐹 ∪ {𝐴}))) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ (ran 𝐹 ∪ {𝐴}) ↔ {𝐴} ⊆ (ran 𝐹 ∪ {𝐴}))) |
9 | 2, 8 | mpbiri 248 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ (ran 𝐹 ∪ {𝐴})) |
10 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) → 𝐴 ∈ (ran 𝐹 ∪ {𝐴})) |
11 | 1, 10 | sseldd 3604 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) → 𝐴 ∈ ∪ 𝑢) |
12 | | eluni2 4440 |
. . . . . 6
⊢ (𝐴 ∈ ∪ 𝑢
↔ ∃𝑤 ∈
𝑢 𝐴 ∈ 𝑤) |
13 | 11, 12 | sylib 208 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) → ∃𝑤 ∈ 𝑢 𝐴 ∈ 𝑤) |
14 | | nnuz 11723 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
15 | | simprr 796 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ (𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤)) → 𝐴 ∈ 𝑤) |
16 | | 1zzd 11408 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ (𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤)) → 1 ∈ ℤ) |
17 | 4 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ (𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤)) → 𝐹(⇝𝑡‘𝐽)𝐴) |
18 | | simplrl 800 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ (𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤)) → 𝑢 ∈ 𝒫 𝐽) |
19 | 18 | elpwid 4170 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ (𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤)) → 𝑢 ⊆ 𝐽) |
20 | | simprl 794 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ (𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤)) → 𝑤 ∈ 𝑢) |
21 | 19, 20 | sseldd 3604 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ (𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤)) → 𝑤 ∈ 𝐽) |
22 | 14, 15, 16, 17, 21 | lmcvg 21066 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ (𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤) |
23 | | imassrn 5477 |
. . . . . . . . . . . . 13
⊢ (𝐹 “ (1...𝑗)) ⊆ ran 𝐹 |
24 | | ssun1 3776 |
. . . . . . . . . . . . 13
⊢ ran 𝐹 ⊆ (ran 𝐹 ∪ {𝐴}) |
25 | 23, 24 | sstri 3612 |
. . . . . . . . . . . 12
⊢ (𝐹 “ (1...𝑗)) ⊆ (ran 𝐹 ∪ {𝐴}) |
26 | | id 22 |
. . . . . . . . . . . 12
⊢ ((ran
𝐹 ∪ {𝐴}) ⊆ ∪
𝑢 → (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢) |
27 | 25, 26 | syl5ss 3614 |
. . . . . . . . . . 11
⊢ ((ran
𝐹 ∪ {𝐴}) ⊆ ∪
𝑢 → (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑢) |
28 | | 1stckgen.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:ℕ⟶𝑋) |
29 | | frn 6053 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:ℕ⟶𝑋 → ran 𝐹 ⊆ 𝑋) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ran 𝐹 ⊆ 𝑋) |
31 | 23, 30 | syl5ss 3614 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐹 “ (1...𝑗)) ⊆ 𝑋) |
32 | | resttopon 20965 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹 “ (1...𝑗)) ⊆ 𝑋) → (𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ (TopOn‘(𝐹 “ (1...𝑗)))) |
33 | 3, 31, 32 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ (TopOn‘(𝐹 “ (1...𝑗)))) |
34 | | topontop 20718 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ (TopOn‘(𝐹 “ (1...𝑗))) → (𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ Top) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ Top) |
36 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1...𝑗) ∈ Fin) |
37 | | ffun 6048 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹:ℕ⟶𝑋 → Fun 𝐹) |
38 | 28, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Fun 𝐹) |
39 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ) |
40 | 39 | ssriv 3607 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...𝑗) ⊆
ℕ |
41 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹:ℕ⟶𝑋 → dom 𝐹 = ℕ) |
42 | 28, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → dom 𝐹 = ℕ) |
43 | 40, 42 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1...𝑗) ⊆ dom 𝐹) |
44 | | fores 6124 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐹 ∧ (1...𝑗) ⊆ dom 𝐹) → (𝐹 ↾ (1...𝑗)):(1...𝑗)–onto→(𝐹 “ (1...𝑗))) |
45 | 38, 43, 44 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹 ↾ (1...𝑗)):(1...𝑗)–onto→(𝐹 “ (1...𝑗))) |
46 | | fofi 8252 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1...𝑗) ∈ Fin
∧ (𝐹 ↾ (1...𝑗)):(1...𝑗)–onto→(𝐹 “ (1...𝑗))) → (𝐹 “ (1...𝑗)) ∈ Fin) |
47 | 36, 45, 46 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐹 “ (1...𝑗)) ∈ Fin) |
48 | | pwfi 8261 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 “ (1...𝑗)) ∈ Fin ↔ 𝒫 (𝐹 “ (1...𝑗)) ∈ Fin) |
49 | 47, 48 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝒫 (𝐹 “ (1...𝑗)) ∈ Fin) |
50 | | restsspw 16092 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ↾t (𝐹 “ (1...𝑗))) ⊆ 𝒫 (𝐹 “ (1...𝑗)) |
51 | | ssfi 8180 |
. . . . . . . . . . . . . . . 16
⊢
((𝒫 (𝐹
“ (1...𝑗)) ∈ Fin
∧ (𝐽
↾t (𝐹
“ (1...𝑗))) ⊆
𝒫 (𝐹 “
(1...𝑗))) → (𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ Fin) |
52 | 49, 50, 51 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ Fin) |
53 | 35, 52 | elind 3798 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ (Top ∩ Fin)) |
54 | | fincmp 21196 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ (Top ∩ Fin) → (𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ Comp) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ Comp) |
56 | | topontop 20718 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
57 | 3, 56 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐽 ∈ Top) |
58 | | toponuni 20719 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
59 | 3, 58 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
60 | 31, 59 | sseqtrd 3641 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 “ (1...𝑗)) ⊆ ∪ 𝐽) |
61 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝐽 =
∪ 𝐽 |
62 | 61 | cmpsub 21203 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝐽) → ((𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐽((𝐹 “ (1...𝑗)) ⊆ ∪ 𝑢 → ∃𝑠 ∈ (𝒫 𝑢 ∩ Fin)(𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠))) |
63 | 57, 60, 62 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐽 ↾t (𝐹 “ (1...𝑗))) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐽((𝐹 “ (1...𝑗)) ⊆ ∪ 𝑢 → ∃𝑠 ∈ (𝒫 𝑢 ∩ Fin)(𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠))) |
64 | 55, 63 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑢 ∈ 𝒫 𝐽((𝐹 “ (1...𝑗)) ⊆ ∪ 𝑢 → ∃𝑠 ∈ (𝒫 𝑢 ∩ Fin)(𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) |
65 | 64 | r19.21bi 2932 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝒫 𝐽) → ((𝐹 “ (1...𝑗)) ⊆ ∪ 𝑢 → ∃𝑠 ∈ (𝒫 𝑢 ∩ Fin)(𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) |
66 | 27, 65 | syl5 34 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝒫 𝐽) → ((ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢 → ∃𝑠 ∈ (𝒫 𝑢 ∩ Fin)(𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) |
67 | 66 | impr 649 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) → ∃𝑠 ∈ (𝒫 𝑢 ∩ Fin)(𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠) |
68 | 67 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) → ∃𝑠 ∈ (𝒫 𝑢 ∩ Fin)(𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠) |
69 | | inss1 3833 |
. . . . . . . . . . . . . 14
⊢
(𝒫 𝑢 ∩
Fin) ⊆ 𝒫 𝑢 |
70 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → 𝑠 ∈ (𝒫 𝑢 ∩ Fin)) |
71 | 69, 70 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → 𝑠 ∈ 𝒫 𝑢) |
72 | 71 | elpwid 4170 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → 𝑠 ⊆ 𝑢) |
73 | | simprll 802 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) → 𝑤 ∈ 𝑢) |
74 | 73 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → 𝑤 ∈ 𝑢) |
75 | 74 | snssd 4340 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → {𝑤} ⊆ 𝑢) |
76 | 72, 75 | unssd 3789 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → (𝑠 ∪ {𝑤}) ⊆ 𝑢) |
77 | | vex 3203 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
78 | 77 | elpw2 4828 |
. . . . . . . . . . 11
⊢ ((𝑠 ∪ {𝑤}) ∈ 𝒫 𝑢 ↔ (𝑠 ∪ {𝑤}) ⊆ 𝑢) |
79 | 76, 78 | sylibr 224 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → (𝑠 ∪ {𝑤}) ∈ 𝒫 𝑢) |
80 | | inss2 3834 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑢 ∩
Fin) ⊆ Fin |
81 | 80, 70 | sseldi 3601 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → 𝑠 ∈ Fin) |
82 | | snfi 8038 |
. . . . . . . . . . 11
⊢ {𝑤} ∈ Fin |
83 | | unfi 8227 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ Fin ∧ {𝑤} ∈ Fin) → (𝑠 ∪ {𝑤}) ∈ Fin) |
84 | 81, 82, 83 | sylancl 694 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → (𝑠 ∪ {𝑤}) ∈ Fin) |
85 | 79, 84 | elind 3798 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → (𝑠 ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin)) |
86 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℕ⟶𝑋 → 𝐹 Fn ℕ) |
87 | 28, 86 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn ℕ) |
88 | 87 | ad3antrrr 766 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → 𝐹 Fn ℕ) |
89 | | simprrr 805 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤) |
90 | 89 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤) |
91 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
92 | 91 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ∈ 𝑤 ↔ (𝐹‘𝑛) ∈ 𝑤)) |
93 | 92 | rspccva 3308 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑛) ∈ 𝑤) |
94 | 90, 93 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑛) ∈ 𝑤) |
95 | | elun2 3781 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑛) ∈ 𝑤 → (𝐹‘𝑛) ∈ (∪ 𝑠 ∪ 𝑤)) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑛) ∈ (∪ 𝑠 ∪ 𝑤)) |
97 | 96 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑛) ∈ (∪ 𝑠 ∪ 𝑤)) |
98 | | elnnuz 11724 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
99 | 98 | anbi1i 731 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑛)) ↔ (𝑛 ∈ (ℤ≥‘1)
∧ 𝑗 ∈
(ℤ≥‘𝑛))) |
100 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑗) ↔ (𝑛 ∈ (ℤ≥‘1)
∧ 𝑗 ∈
(ℤ≥‘𝑛))) |
101 | 99, 100 | bitr4i 267 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑛)) ↔ 𝑛 ∈ (1...𝑗)) |
102 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠) |
103 | | funimass4 6247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
𝐹 ∧ (1...𝑗) ⊆ dom 𝐹) → ((𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠 ↔ ∀𝑛 ∈ (1...𝑗)(𝐹‘𝑛) ∈ ∪ 𝑠)) |
104 | 38, 43, 103 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠 ↔ ∀𝑛 ∈ (1...𝑗)(𝐹‘𝑛) ∈ ∪ 𝑠)) |
105 | 104 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → ((𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠 ↔ ∀𝑛 ∈ (1...𝑗)(𝐹‘𝑛) ∈ ∪ 𝑠)) |
106 | 102, 105 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → ∀𝑛 ∈ (1...𝑗)(𝐹‘𝑛) ∈ ∪ 𝑠) |
107 | 106 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) ∧ 𝑛 ∈ (1...𝑗)) → (𝐹‘𝑛) ∈ ∪ 𝑠) |
108 | | elun1 3780 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑛) ∈ ∪ 𝑠 → (𝐹‘𝑛) ∈ (∪ 𝑠 ∪ 𝑤)) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) ∧ 𝑛 ∈ (1...𝑗)) → (𝐹‘𝑛) ∈ (∪ 𝑠 ∪ 𝑤)) |
110 | 101, 109 | sylan2b 492 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) ∧ (𝑛 ∈ ℕ ∧ 𝑗 ∈ (ℤ≥‘𝑛))) → (𝐹‘𝑛) ∈ (∪ 𝑠 ∪ 𝑤)) |
111 | 110 | anassrs 680 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑛) ∈ (∪ 𝑠 ∪ 𝑤)) |
112 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤)) → 𝑗 ∈ ℕ) |
113 | 112 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → 𝑗 ∈ ℕ) |
114 | | nnz 11399 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
115 | | nnz 11399 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
116 | | uztric 11709 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑛 ∈
(ℤ≥‘𝑗) ∨ 𝑗 ∈ (ℤ≥‘𝑛))) |
117 | 114, 115,
116 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑛 ∈
(ℤ≥‘𝑗) ∨ 𝑗 ∈ (ℤ≥‘𝑛))) |
118 | 113, 117 | sylan 488 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) ∧ 𝑛 ∈ ℕ) → (𝑛 ∈ (ℤ≥‘𝑗) ∨ 𝑗 ∈ (ℤ≥‘𝑛))) |
119 | 97, 111, 118 | mpjaodan 827 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (∪ 𝑠 ∪ 𝑤)) |
120 | 119 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (∪ 𝑠 ∪ 𝑤)) |
121 | | fnfvrnss 6390 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (∪ 𝑠 ∪ 𝑤)) → ran 𝐹 ⊆ (∪ 𝑠 ∪ 𝑤)) |
122 | 88, 120, 121 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → ran 𝐹 ⊆ (∪ 𝑠 ∪ 𝑤)) |
123 | | elun2 3781 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑤 → 𝐴 ∈ (∪ 𝑠 ∪ 𝑤)) |
124 | 123 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤)) → 𝐴 ∈ (∪ 𝑠 ∪ 𝑤)) |
125 | 124 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → 𝐴 ∈ (∪ 𝑠 ∪ 𝑤)) |
126 | 125 | snssd 4340 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → {𝐴} ⊆ (∪
𝑠 ∪ 𝑤)) |
127 | 122, 126 | unssd 3789 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → (ran 𝐹 ∪ {𝐴}) ⊆ (∪
𝑠 ∪ 𝑤)) |
128 | | uniun 4456 |
. . . . . . . . . . 11
⊢ ∪ (𝑠
∪ {𝑤}) = (∪ 𝑠
∪ ∪ {𝑤}) |
129 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑤 ∈ V |
130 | 129 | unisn 4451 |
. . . . . . . . . . . 12
⊢ ∪ {𝑤}
= 𝑤 |
131 | 130 | uneq2i 3764 |
. . . . . . . . . . 11
⊢ (∪ 𝑠
∪ ∪ {𝑤}) = (∪ 𝑠 ∪ 𝑤) |
132 | 128, 131 | eqtri 2644 |
. . . . . . . . . 10
⊢ ∪ (𝑠
∪ {𝑤}) = (∪ 𝑠
∪ 𝑤) |
133 | 127, 132 | syl6sseqr 3652 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → (ran 𝐹 ∪ {𝐴}) ⊆ ∪
(𝑠 ∪ {𝑤})) |
134 | | unieq 4444 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑠 ∪ {𝑤}) → ∪ 𝑣 = ∪
(𝑠 ∪ {𝑤})) |
135 | 134 | sseq2d 3633 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑠 ∪ {𝑤}) → ((ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣 ↔ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
(𝑠 ∪ {𝑤}))) |
136 | 135 | rspcev 3309 |
. . . . . . . . 9
⊢ (((𝑠 ∪ {𝑤}) ∈ (𝒫 𝑢 ∩ Fin) ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
(𝑠 ∪ {𝑤})) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)(ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣) |
137 | 85, 133, 136 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) ∧ (𝑠 ∈ (𝒫 𝑢 ∩ Fin) ∧ (𝐹 “ (1...𝑗)) ⊆ ∪ 𝑠)) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)(ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣) |
138 | 68, 137 | rexlimddv 3035 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ ((𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤))) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)(ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣) |
139 | 138 | anassrs 680 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ (𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤)) ∧ (𝑗 ∈ ℕ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑤)) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)(ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣) |
140 | 22, 139 | rexlimddv 3035 |
. . . . 5
⊢ (((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) ∧ (𝑤 ∈ 𝑢 ∧ 𝐴 ∈ 𝑤)) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)(ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣) |
141 | 13, 140 | rexlimddv 3035 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢)) → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)(ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣) |
142 | 141 | expr 643 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝒫 𝐽) → ((ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)(ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣)) |
143 | 142 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ 𝒫 𝐽((ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)(ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣)) |
144 | 6 | snssd 4340 |
. . . . 5
⊢ (𝜑 → {𝐴} ⊆ 𝑋) |
145 | 30, 144 | unssd 3789 |
. . . 4
⊢ (𝜑 → (ran 𝐹 ∪ {𝐴}) ⊆ 𝑋) |
146 | 145, 59 | sseqtrd 3641 |
. . 3
⊢ (𝜑 → (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝐽) |
147 | 61 | cmpsub 21203 |
. . 3
⊢ ((𝐽 ∈ Top ∧ (ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝐽) → ((𝐽 ↾t (ran 𝐹 ∪ {𝐴})) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐽((ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)(ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣))) |
148 | 57, 146, 147 | syl2anc 693 |
. 2
⊢ (𝜑 → ((𝐽 ↾t (ran 𝐹 ∪ {𝐴})) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐽((ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)(ran 𝐹 ∪ {𝐴}) ⊆ ∪
𝑣))) |
149 | 143, 148 | mpbird 247 |
1
⊢ (𝜑 → (𝐽 ↾t (ran 𝐹 ∪ {𝐴})) ∈ Comp) |