Step | Hyp | Ref
| Expression |
1 | | ptcls.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | ptcls.j |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑅 ∈ (TopOn‘𝑋)) |
3 | | topontop 20541 |
. . . . . 6
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑅 ∈ Top) |
5 | | ptcls.c |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ 𝑋) |
6 | | toponuni 20542 |
. . . . . . . 8
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑅) |
7 | 2, 6 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 = ∪ 𝑅) |
8 | 5, 7 | sseqtrd 3604 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ ∪ 𝑅) |
9 | | eqid 2610 |
. . . . . . 7
⊢ ∪ 𝑅 =
∪ 𝑅 |
10 | 9 | clscld 20661 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅)
→ ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝑅)) |
11 | 4, 8, 10 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝑅)) |
12 | 1, 4, 11 | ptcldmpt 21227 |
. . . 4
⊢ (𝜑 → X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ∈
(Clsd‘(∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅)))) |
13 | | ptcls.2 |
. . . . 5
⊢ 𝐽 =
(∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅)) |
14 | 13 | fveq2i 6106 |
. . . 4
⊢
(Clsd‘𝐽) =
(Clsd‘(∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅))) |
15 | 12, 14 | syl6eleqr 2699 |
. . 3
⊢ (𝜑 → X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝐽)) |
16 | 9 | sscls 20670 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅)
→ 𝑆 ⊆
((cls‘𝑅)‘𝑆)) |
17 | 4, 8, 16 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ ((cls‘𝑅)‘𝑆)) |
18 | 17 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑆 ⊆ ((cls‘𝑅)‘𝑆)) |
19 | | ss2ixp 7807 |
. . . 4
⊢
(∀𝑘 ∈
𝐴 𝑆 ⊆ ((cls‘𝑅)‘𝑆) → X𝑘 ∈ 𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (𝜑 → X𝑘 ∈
𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) |
21 | | eqid 2610 |
. . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 |
22 | 21 | clsss2 20686 |
. . 3
⊢ ((X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝐽) ∧ X𝑘 ∈ 𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆) ⊆ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) |
23 | 15, 20, 22 | syl2anc 691 |
. 2
⊢ (𝜑 → ((cls‘𝐽)‘X𝑘 ∈
𝐴 𝑆) ⊆ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) |
24 | | vex 3176 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
25 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) ↔ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))) |
26 | 25 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → (((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ↔ ((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)))) |
27 | 26 | exbidv 1837 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)))) |
28 | 24, 27 | elab 3319 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))) |
29 | | nffvmpt1 6111 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) |
30 | 29 | nfel2 2767 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘(𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) |
31 | | nfv 1830 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦(𝑔‘𝑘) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘) |
32 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑘 → (𝑔‘𝑦) = (𝑔‘𝑘)) |
33 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑘 → ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) = ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘)) |
34 | 32, 33 | eleq12d 2682 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑘 → ((𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ↔ (𝑔‘𝑘) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘))) |
35 | 30, 31, 34 | cbvral 3143 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ↔ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘)) |
36 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴) |
37 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝐴 ↦ 𝑅) = (𝑘 ∈ 𝐴 ↦ 𝑅) |
38 | 37 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ 𝐴 ∧ 𝑅 ∈ (TopOn‘𝑋)) → ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘) = 𝑅) |
39 | 36, 2, 38 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘) = 𝑅) |
40 | 39 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑔‘𝑘) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘) ↔ (𝑔‘𝑘) ∈ 𝑅)) |
41 | 40 | ralbidva 2968 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅)) |
42 | 35, 41 | syl5bb 271 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ↔ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅)) |
43 | 42 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ↔ (𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅))) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → ((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ↔ (𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅))) |
45 | 44 | biimpa 500 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦))) → (𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅)) |
46 | | ptclsg.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝑆 ∈ AC 𝐴) |
47 | 46 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∪ 𝑘 ∈ 𝐴 𝑆 ∈ AC 𝐴) |
48 | | simpll 786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → 𝜑) |
49 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑓 ∈ V |
50 | 49 | elixp 7801 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆))) |
51 | 50 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆)) |
52 | 51 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆)) |
53 | 9 | clsndisj 20689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅
∧ (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆)) ∧ ((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘))) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅) |
54 | 53 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅
∧ (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆)) → (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅)) |
55 | 54 | 3expia 1259 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅)
→ ((𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆) → (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅))) |
56 | 4, 8, 55 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆) → (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅))) |
57 | 56 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆) → ∀𝑘 ∈ 𝐴 (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅))) |
58 | 48, 52, 57 | sylc 63 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅)) |
59 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) |
60 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦)) |
61 | 32 | cbvixpv 7812 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ X𝑦 ∈
𝐴 (𝑔‘𝑦) = X𝑘 ∈ 𝐴 (𝑔‘𝑘) |
62 | 60, 61 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → 𝑓 ∈ X𝑘 ∈ 𝐴 (𝑔‘𝑘)) |
63 | 49 | elixp 7801 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 (𝑔‘𝑘) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (𝑔‘𝑘))) |
64 | 63 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 (𝑔‘𝑘) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (𝑔‘𝑘)) |
65 | 62, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (𝑔‘𝑘)) |
66 | | r19.26 3046 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑘 ∈
𝐴 ((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) ↔ (∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (𝑔‘𝑘))) |
67 | 59, 65, 66 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘))) |
68 | | ralim 2932 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑘 ∈
𝐴 (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅) → (∀𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ∀𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅)) |
69 | 58, 67, 68 | sylc 63 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅) |
70 | | rabn0 3912 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑧 ∈ ∪ 𝑘 ∈ 𝐴 𝑆 ∣ 𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)} ≠ ∅ ↔ ∃𝑧 ∈ ∪ 𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)) |
71 | | dfin5 3548 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∪ 𝑘 ∈ 𝐴 𝑆 ∩ ((𝑔‘𝑘) ∩ 𝑆)) = {𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆 ∣ 𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)} |
72 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔‘𝑘) ∩ 𝑆) ⊆ 𝑆 |
73 | | ssiun2 4499 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ 𝐴 → 𝑆 ⊆ ∪
𝑘 ∈ 𝐴 𝑆) |
74 | 72, 73 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝐴 → ((𝑔‘𝑘) ∩ 𝑆) ⊆ ∪ 𝑘 ∈ 𝐴 𝑆) |
75 | | sseqin2 3779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑔‘𝑘) ∩ 𝑆) ⊆ ∪ 𝑘 ∈ 𝐴 𝑆 ↔ (∪
𝑘 ∈ 𝐴 𝑆 ∩ ((𝑔‘𝑘) ∩ 𝑆)) = ((𝑔‘𝑘) ∩ 𝑆)) |
76 | 74, 75 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝐴 → (∪
𝑘 ∈ 𝐴 𝑆 ∩ ((𝑔‘𝑘) ∩ 𝑆)) = ((𝑔‘𝑘) ∩ 𝑆)) |
77 | 71, 76 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝐴 → {𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆 ∣ 𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)} = ((𝑔‘𝑘) ∩ 𝑆)) |
78 | 77 | neeq1d 2841 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ 𝐴 → ({𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆 ∣ 𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)} ≠ ∅ ↔ ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅)) |
79 | 70, 78 | syl5bbr 273 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝐴 → (∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅)) |
80 | 79 | ralbiia 2962 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ ∀𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅) |
81 | 69, 80 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)) |
82 | | nfv 1830 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦∃𝑧 ∈ ∪ 𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) |
83 | | nfiu1 4486 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘∪ 𝑘 ∈ 𝐴 𝑆 |
84 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑘(𝑔‘𝑦) |
85 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌𝑆 |
86 | 84, 85 | nfin 3782 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆) |
87 | 86 | nfel2 2767 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘 𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆) |
88 | 83, 87 | nfrex 2990 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘∃𝑧 ∈ ∪ 𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆) |
89 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑦 → (𝑔‘𝑘) = (𝑔‘𝑦)) |
90 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑦 → 𝑆 = ⦋𝑦 / 𝑘⦌𝑆) |
91 | 89, 90 | ineq12d 3777 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → ((𝑔‘𝑘) ∩ 𝑆) = ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) |
92 | 91 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → (𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ 𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) |
93 | 92 | rexbidv 3034 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → (∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) |
94 | 82, 88, 93 | cbvral 3143 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘 ∈
𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) |
95 | 81, 94 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) |
96 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (ℎ‘𝑦) → (𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆) ↔ (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) |
97 | 96 | acni3 8753 |
. . . . . . . . . . . . . . 15
⊢
((∪ 𝑘 ∈ 𝐴 𝑆 ∈ AC 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) → ∃ℎ(ℎ:𝐴⟶∪
𝑘 ∈ 𝐴 𝑆 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) |
98 | 47, 95, 97 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∃ℎ(ℎ:𝐴⟶∪
𝑘 ∈ 𝐴 𝑆 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) |
99 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ:𝐴⟶∪
𝑘 ∈ 𝐴 𝑆 → ℎ Fn 𝐴) |
100 | | nfv 1830 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦(ℎ‘𝑘) ∈ ((𝑔‘𝑘) ∩ 𝑆) |
101 | 86 | nfel2 2767 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘(ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆) |
102 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (ℎ‘𝑘) = (ℎ‘𝑦)) |
103 | 102, 91 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → ((ℎ‘𝑘) ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) |
104 | 100, 101,
103 | cbvral 3143 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
𝐴 (ℎ‘𝑘) ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) |
105 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ ∈ X𝑘 ∈
𝐴 ((𝑔‘𝑘) ∩ 𝑆) → X𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅) |
106 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℎ ∈ V |
107 | 106 | elixp 7801 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ ∈ X𝑘 ∈
𝐴 ((𝑔‘𝑘) ∩ 𝑆) ↔ (ℎ Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (ℎ‘𝑘) ∈ ((𝑔‘𝑘) ∩ 𝑆))) |
108 | | ixpin 7819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ X𝑘 ∈
𝐴 ((𝑔‘𝑘) ∩ 𝑆) = (X𝑘 ∈ 𝐴 (𝑔‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) |
109 | 61 | ineq1i 3772 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (X𝑦 ∈
𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) = (X𝑘 ∈ 𝐴 (𝑔‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) |
110 | 108, 109 | eqtr4i 2635 |
. . . . . . . . . . . . . . . . . . 19
⊢ X𝑘 ∈
𝐴 ((𝑔‘𝑘) ∩ 𝑆) = (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) |
111 | 110 | neeq1i 2846 |
. . . . . . . . . . . . . . . . . 18
⊢ (X𝑘 ∈
𝐴 ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅ ↔ (X𝑦 ∈
𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) |
112 | 105, 107,
111 | 3imtr3i 279 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (ℎ‘𝑘) ∈ ((𝑔‘𝑘) ∩ 𝑆)) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) |
113 | 104, 112 | sylan2br 492 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) |
114 | 99, 113 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ:𝐴⟶∪
𝑘 ∈ 𝐴 𝑆 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) |
115 | 114 | exlimiv 1845 |
. . . . . . . . . . . . . 14
⊢
(∃ℎ(ℎ:𝐴⟶∪
𝑘 ∈ 𝐴 𝑆 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) |
116 | 98, 115 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) |
117 | 116 | expr 641 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅)) → (𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅)) |
118 | 45, 117 | syldan 486 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦))) → (𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅)) |
119 | 118 | 3adantr3 1215 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦))) → (𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅)) |
120 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (𝑓 ∈ 𝑢 ↔ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) |
121 | | ineq1 3769 |
. . . . . . . . . . . 12
⊢ (𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) = (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆)) |
122 | 121 | neeq1d 2841 |
. . . . . . . . . . 11
⊢ (𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅ ↔ (X𝑦 ∈
𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅)) |
123 | 120, 122 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) ↔ (𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) |
124 | 119, 123 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦))) → (𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) |
125 | 124 | expimpd 627 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → (((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) |
126 | 125 | exlimdv 1848 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) |
127 | 28, 126 | syl5bi 231 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → (𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} → (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) |
128 | 127 | ralrimiv 2948 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → ∀𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅)) |
129 | 4, 37 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑅):𝐴⟶Top) |
130 | | ffn 5958 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝐴 ↦ 𝑅):𝐴⟶Top → (𝑘 ∈ 𝐴 ↦ 𝑅) Fn 𝐴) |
131 | 129, 130 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑅) Fn 𝐴) |
132 | | eqid 2610 |
. . . . . . . . . 10
⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} |
133 | 132 | ptval 21183 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ 𝑅) Fn 𝐴) → (∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅)) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
134 | 1, 131, 133 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 →
(∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅)) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
135 | 13, 134 | syl5eq 2656 |
. . . . . . 7
⊢ (𝜑 → 𝐽 = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
136 | 135 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → 𝐽 = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
137 | 2 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑅 ∈ (TopOn‘𝑋)) |
138 | 13 | pttopon 21209 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝑅 ∈ (TopOn‘𝑋)) → 𝐽 ∈ (TopOn‘X𝑘 ∈
𝐴 𝑋)) |
139 | 1, 137, 138 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (TopOn‘X𝑘 ∈
𝐴 𝑋)) |
140 | | toponuni 20542 |
. . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘X𝑘 ∈
𝐴 𝑋) → X𝑘 ∈ 𝐴 𝑋 = ∪ 𝐽) |
141 | 139, 140 | syl 17 |
. . . . . . 7
⊢ (𝜑 → X𝑘 ∈
𝐴 𝑋 = ∪ 𝐽) |
142 | 141 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → X𝑘 ∈ 𝐴 𝑋 = ∪ 𝐽) |
143 | 132 | ptbas 21192 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ 𝑅):𝐴⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ∈ TopBases) |
144 | 1, 129, 143 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ∈ TopBases) |
145 | 144 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ∈ TopBases) |
146 | 5 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑆 ⊆ 𝑋) |
147 | | ss2ixp 7807 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 𝑆 ⊆ 𝑋 → X𝑘 ∈ 𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 𝑋) |
148 | 146, 147 | syl 17 |
. . . . . . 7
⊢ (𝜑 → X𝑘 ∈
𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 𝑋) |
149 | 148 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → X𝑘 ∈ 𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 𝑋) |
150 | 9 | clsss3 20673 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅)
→ ((cls‘𝑅)‘𝑆) ⊆ ∪ 𝑅) |
151 | 4, 8, 150 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((cls‘𝑅)‘𝑆) ⊆ ∪ 𝑅) |
152 | 151, 7 | sseqtr4d 3605 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((cls‘𝑅)‘𝑆) ⊆ 𝑋) |
153 | 152 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆) ⊆ 𝑋) |
154 | | ss2ixp 7807 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ⊆ 𝑋 → X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆) ⊆ X𝑘 ∈ 𝐴 𝑋) |
155 | 153, 154 | syl 17 |
. . . . . . 7
⊢ (𝜑 → X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ⊆ X𝑘 ∈ 𝐴 𝑋) |
156 | 155 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → 𝑓 ∈ X𝑘 ∈ 𝐴 𝑋) |
157 | 136, 142,
145, 149, 156 | elcls3 20697 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → (𝑓 ∈ ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆) ↔ ∀𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) |
158 | 128, 157 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → 𝑓 ∈ ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆)) |
159 | 158 | ex 449 |
. . 3
⊢ (𝜑 → (𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆) → 𝑓 ∈ ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆))) |
160 | 159 | ssrdv 3574 |
. 2
⊢ (𝜑 → X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ⊆ ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆)) |
161 | 23, 160 | eqssd 3585 |
1
⊢ (𝜑 → ((cls‘𝐽)‘X𝑘 ∈
𝐴 𝑆) = X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) |