Step | Hyp | Ref
| Expression |
1 | | txtube.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ Comp) |
2 | | txtube.u |
. . . . . . . 8
⊢ (𝜑 → (𝑋 × {𝐴}) ⊆ 𝑈) |
3 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑋 × {𝐴}) ⊆ 𝑈) |
4 | | id 22 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑋 → 𝑥 ∈ 𝑋) |
5 | | txtube.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑌) |
6 | | snidg 4153 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑌 → 𝐴 ∈ {𝐴}) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
8 | | opelxpi 5072 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∧ 𝐴 ∈ {𝐴}) → 〈𝑥, 𝐴〉 ∈ (𝑋 × {𝐴})) |
9 | 4, 7, 8 | syl2anr 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 〈𝑥, 𝐴〉 ∈ (𝑋 × {𝐴})) |
10 | 3, 9 | sseldd 3569 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 〈𝑥, 𝐴〉 ∈ 𝑈) |
11 | | txtube.w |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ (𝑅 ×t 𝑆)) |
12 | | txtube.s |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ Top) |
13 | | eltx 21181 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Comp ∧ 𝑆 ∈ Top) → (𝑈 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑈 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
14 | 1, 12, 13 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑈 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑈 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
15 | 11, 14 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝑈 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)) |
16 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑈 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)) |
17 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑥, 𝐴〉 → (𝑦 ∈ (𝑢 × 𝑣) ↔ 〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣))) |
18 | 17 | anbi1d 737 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑥, 𝐴〉 → ((𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
19 | 18 | 2rexbidv 3039 |
. . . . . . 7
⊢ (𝑦 = 〈𝑥, 𝐴〉 → (∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
20 | 19 | rspcv 3278 |
. . . . . 6
⊢
(〈𝑥, 𝐴〉 ∈ 𝑈 → (∀𝑦 ∈ 𝑈 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) → ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
21 | 10, 16, 20 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)) |
22 | | opelxp 5070 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣) ↔ (𝑥 ∈ 𝑢 ∧ 𝐴 ∈ 𝑣)) |
23 | 22 | anbi1i 727 |
. . . . . . . . 9
⊢
((〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ((𝑥 ∈ 𝑢 ∧ 𝐴 ∈ 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈)) |
24 | | anass 679 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝑢 ∧ 𝐴 ∈ 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝑥 ∈ 𝑢 ∧ (𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
25 | 23, 24 | bitri 263 |
. . . . . . . 8
⊢
((〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝑥 ∈ 𝑢 ∧ (𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
26 | 25 | rexbii 3023 |
. . . . . . 7
⊢
(∃𝑣 ∈
𝑆 (〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ∃𝑣 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ (𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
27 | | r19.42v 3073 |
. . . . . . 7
⊢
(∃𝑣 ∈
𝑆 (𝑥 ∈ 𝑢 ∧ (𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈)) ↔ (𝑥 ∈ 𝑢 ∧ ∃𝑣 ∈ 𝑆 (𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
28 | 26, 27 | bitri 263 |
. . . . . 6
⊢
(∃𝑣 ∈
𝑆 (〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝑥 ∈ 𝑢 ∧ ∃𝑣 ∈ 𝑆 (𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
29 | 28 | rexbii 3023 |
. . . . 5
⊢
(∃𝑢 ∈
𝑅 ∃𝑣 ∈ 𝑆 (〈𝑥, 𝐴〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ ∃𝑢 ∈ 𝑅 (𝑥 ∈ 𝑢 ∧ ∃𝑣 ∈ 𝑆 (𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
30 | 21, 29 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑢 ∈ 𝑅 (𝑥 ∈ 𝑢 ∧ ∃𝑣 ∈ 𝑆 (𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
31 | 30 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑅 (𝑥 ∈ 𝑢 ∧ ∃𝑣 ∈ 𝑆 (𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) |
32 | | txtube.x |
. . . 4
⊢ 𝑋 = ∪
𝑅 |
33 | | eleq2 2677 |
. . . . 5
⊢ (𝑣 = (𝑓‘𝑢) → (𝐴 ∈ 𝑣 ↔ 𝐴 ∈ (𝑓‘𝑢))) |
34 | | xpeq2 5053 |
. . . . . 6
⊢ (𝑣 = (𝑓‘𝑢) → (𝑢 × 𝑣) = (𝑢 × (𝑓‘𝑢))) |
35 | 34 | sseq1d 3595 |
. . . . 5
⊢ (𝑣 = (𝑓‘𝑢) → ((𝑢 × 𝑣) ⊆ 𝑈 ↔ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)) |
36 | 33, 35 | anbi12d 743 |
. . . 4
⊢ (𝑣 = (𝑓‘𝑢) → ((𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈) ↔ (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈))) |
37 | 32, 36 | cmpcovf 21004 |
. . 3
⊢ ((𝑅 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑅 (𝑥 ∈ 𝑢 ∧ ∃𝑣 ∈ 𝑆 (𝐴 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ 𝑈))) → ∃𝑡 ∈ (𝒫 𝑅 ∩ Fin)(𝑋 = ∪ 𝑡 ∧ ∃𝑓(𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) |
38 | 1, 31, 37 | syl2anc 691 |
. 2
⊢ (𝜑 → ∃𝑡 ∈ (𝒫 𝑅 ∩ Fin)(𝑋 = ∪ 𝑡 ∧ ∃𝑓(𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) |
39 | | rint0 4452 |
. . . . . . . . . 10
⊢ (ran
𝑓 = ∅ → (𝑌 ∩ ∩ ran 𝑓) = 𝑌) |
40 | 39 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 = ∅) → (𝑌 ∩ ∩ ran
𝑓) = 𝑌) |
41 | | txtube.y |
. . . . . . . . . . . 12
⊢ 𝑌 = ∪
𝑆 |
42 | 41 | topopn 20536 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Top → 𝑌 ∈ 𝑆) |
43 | 12, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝑆) |
44 | 43 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 = ∅) → 𝑌 ∈ 𝑆) |
45 | 40, 44 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 = ∅) → (𝑌 ∩ ∩ ran
𝑓) ∈ 𝑆) |
46 | 12 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → 𝑆 ∈ Top) |
47 | | simprrl 800 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝑓:𝑡⟶𝑆) |
48 | | frn 5966 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝑡⟶𝑆 → ran 𝑓 ⊆ 𝑆) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → ran 𝑓 ⊆ 𝑆) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓 ⊆ 𝑆) |
51 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓 ≠ ∅) |
52 | | inss2 3796 |
. . . . . . . . . . . . . . . 16
⊢
(𝒫 𝑅 ∩
Fin) ⊆ Fin |
53 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) |
54 | 52, 53 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝑡 ∈ Fin) |
55 | | ffn 5958 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝑡⟶𝑆 → 𝑓 Fn 𝑡) |
56 | 47, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝑓 Fn 𝑡) |
57 | | dffn4 6034 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 Fn 𝑡 ↔ 𝑓:𝑡–onto→ran 𝑓) |
58 | 56, 57 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝑓:𝑡–onto→ran 𝑓) |
59 | | fofi 8135 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ Fin ∧ 𝑓:𝑡–onto→ran 𝑓) → ran 𝑓 ∈ Fin) |
60 | 54, 58, 59 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → ran 𝑓 ∈ Fin) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ran 𝑓 ∈ Fin) |
62 | | fiinopn 20531 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ Top → ((ran 𝑓 ⊆ 𝑆 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ∩ ran 𝑓 ∈ 𝑆)) |
63 | 62 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Top ∧ (ran 𝑓 ⊆ 𝑆 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ∩ ran 𝑓 ∈ 𝑆) |
64 | 46, 50, 51, 61, 63 | syl13anc 1320 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ∩ ran 𝑓 ∈ 𝑆) |
65 | | elssuni 4403 |
. . . . . . . . . . . 12
⊢ (∩ ran 𝑓 ∈ 𝑆 → ∩ ran
𝑓 ⊆ ∪ 𝑆) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ∩ ran 𝑓 ⊆ ∪ 𝑆) |
67 | 66, 41 | syl6sseqr 3615 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → ∩ ran 𝑓 ⊆ 𝑌) |
68 | | sseqin2 3779 |
. . . . . . . . . 10
⊢ (∩ ran 𝑓 ⊆ 𝑌 ↔ (𝑌 ∩ ∩ ran
𝑓) = ∩ ran 𝑓) |
69 | 67, 68 | sylib 207 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → (𝑌 ∩ ∩ ran
𝑓) = ∩ ran 𝑓) |
70 | 69, 64 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) ∧ ran 𝑓 ≠ ∅) → (𝑌 ∩ ∩ ran
𝑓) ∈ 𝑆) |
71 | 45, 70 | pm2.61dane 2869 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → (𝑌 ∩ ∩ ran
𝑓) ∈ 𝑆) |
72 | 5 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝐴 ∈ 𝑌) |
73 | | simprrr 801 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)) |
74 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈) → 𝐴 ∈ (𝑓‘𝑢)) |
75 | 74 | ralimi 2936 |
. . . . . . . . . . 11
⊢
(∀𝑢 ∈
𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈) → ∀𝑢 ∈ 𝑡 𝐴 ∈ (𝑓‘𝑢)) |
76 | 73, 75 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → ∀𝑢 ∈ 𝑡 𝐴 ∈ (𝑓‘𝑢)) |
77 | | eliin 4461 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑌 → (𝐴 ∈ ∩
𝑢 ∈ 𝑡 (𝑓‘𝑢) ↔ ∀𝑢 ∈ 𝑡 𝐴 ∈ (𝑓‘𝑢))) |
78 | 72, 77 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → (𝐴 ∈ ∩
𝑢 ∈ 𝑡 (𝑓‘𝑢) ↔ ∀𝑢 ∈ 𝑡 𝐴 ∈ (𝑓‘𝑢))) |
79 | 76, 78 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝐴 ∈ ∩
𝑢 ∈ 𝑡 (𝑓‘𝑢)) |
80 | | fniinfv 6167 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝑡 → ∩
𝑢 ∈ 𝑡 (𝑓‘𝑢) = ∩ ran 𝑓) |
81 | 56, 80 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → ∩ 𝑢 ∈ 𝑡 (𝑓‘𝑢) = ∩ ran 𝑓) |
82 | 79, 81 | eleqtrd 2690 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝐴 ∈ ∩ ran
𝑓) |
83 | 72, 82 | elind 3760 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝐴 ∈ (𝑌 ∩ ∩ ran
𝑓)) |
84 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝑋 = ∪ 𝑡) |
85 | | uniiun 4509 |
. . . . . . . . . . 11
⊢ ∪ 𝑡 =
∪ 𝑢 ∈ 𝑡 𝑢 |
86 | 84, 85 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → 𝑋 = ∪ 𝑢 ∈ 𝑡 𝑢) |
87 | 86 | xpeq1d 5062 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → (𝑋 × (𝑌 ∩ ∩ ran
𝑓)) = (∪ 𝑢 ∈ 𝑡 𝑢 × (𝑌 ∩ ∩ ran
𝑓))) |
88 | | xpiundir 5097 |
. . . . . . . . 9
⊢ (∪ 𝑢 ∈ 𝑡 𝑢 × (𝑌 ∩ ∩ ran
𝑓)) = ∪ 𝑢 ∈ 𝑡 (𝑢 × (𝑌 ∩ ∩ ran
𝑓)) |
89 | 87, 88 | syl6eq 2660 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → (𝑋 × (𝑌 ∩ ∩ ran
𝑓)) = ∪ 𝑢 ∈ 𝑡 (𝑢 × (𝑌 ∩ ∩ ran
𝑓))) |
90 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈) → (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈) |
91 | 90 | ralimi 2936 |
. . . . . . . . . . 11
⊢
(∀𝑢 ∈
𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈) → ∀𝑢 ∈ 𝑡 (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈) |
92 | 73, 91 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → ∀𝑢 ∈ 𝑡 (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈) |
93 | | inss2 3796 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∩ ∩ ran 𝑓) ⊆ ∩ ran
𝑓 |
94 | 80 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡) → ∩
𝑢 ∈ 𝑡 (𝑓‘𝑢) = ∩ ran 𝑓) |
95 | | iinss2 4508 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑡 → ∩
𝑢 ∈ 𝑡 (𝑓‘𝑢) ⊆ (𝑓‘𝑢)) |
96 | 95 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡) → ∩
𝑢 ∈ 𝑡 (𝑓‘𝑢) ⊆ (𝑓‘𝑢)) |
97 | 94, 96 | eqsstr3d 3603 |
. . . . . . . . . . . . 13
⊢ ((𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡) → ∩ ran
𝑓 ⊆ (𝑓‘𝑢)) |
98 | 93, 97 | syl5ss 3579 |
. . . . . . . . . . . 12
⊢ ((𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡) → (𝑌 ∩ ∩ ran
𝑓) ⊆ (𝑓‘𝑢)) |
99 | | xpss2 5152 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∩ ∩ ran 𝑓) ⊆ (𝑓‘𝑢) → (𝑢 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ (𝑢 × (𝑓‘𝑢))) |
100 | | sstr2 3575 |
. . . . . . . . . . . 12
⊢ ((𝑢 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ (𝑢 × (𝑓‘𝑢)) → ((𝑢 × (𝑓‘𝑢)) ⊆ 𝑈 → (𝑢 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈)) |
101 | 98, 99, 100 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡) → ((𝑢 × (𝑓‘𝑢)) ⊆ 𝑈 → (𝑢 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈)) |
102 | 101 | ralimdva 2945 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝑡 → (∀𝑢 ∈ 𝑡 (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈 → ∀𝑢 ∈ 𝑡 (𝑢 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈)) |
103 | 56, 92, 102 | sylc 63 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → ∀𝑢 ∈ 𝑡 (𝑢 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈) |
104 | | iunss 4497 |
. . . . . . . . 9
⊢ (∪ 𝑢 ∈ 𝑡 (𝑢 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈 ↔ ∀𝑢 ∈ 𝑡 (𝑢 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈) |
105 | 103, 104 | sylibr 223 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → ∪ 𝑢 ∈ 𝑡 (𝑢 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈) |
106 | 89, 105 | eqsstrd 3602 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → (𝑋 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈) |
107 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑢 = (𝑌 ∩ ∩ ran
𝑓) → (𝐴 ∈ 𝑢 ↔ 𝐴 ∈ (𝑌 ∩ ∩ ran
𝑓))) |
108 | | xpeq2 5053 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑌 ∩ ∩ ran
𝑓) → (𝑋 × 𝑢) = (𝑋 × (𝑌 ∩ ∩ ran
𝑓))) |
109 | 108 | sseq1d 3595 |
. . . . . . . . 9
⊢ (𝑢 = (𝑌 ∩ ∩ ran
𝑓) → ((𝑋 × 𝑢) ⊆ 𝑈 ↔ (𝑋 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈)) |
110 | 107, 109 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑢 = (𝑌 ∩ ∩ ran
𝑓) → ((𝐴 ∈ 𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈) ↔ (𝐴 ∈ (𝑌 ∩ ∩ ran
𝑓) ∧ (𝑋 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈))) |
111 | 110 | rspcev 3282 |
. . . . . . 7
⊢ (((𝑌 ∩ ∩ ran 𝑓) ∈ 𝑆 ∧ (𝐴 ∈ (𝑌 ∩ ∩ ran
𝑓) ∧ (𝑋 × (𝑌 ∩ ∩ ran
𝑓)) ⊆ 𝑈)) → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)) |
112 | 71, 83, 106, 111 | syl12anc 1316 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ (𝑋 = ∪ 𝑡 ∧ (𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)))) → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)) |
113 | 112 | expr 641 |
. . . . 5
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ 𝑋 = ∪ 𝑡) → ((𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)) → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))) |
114 | 113 | exlimdv 1848 |
. . . 4
⊢ (((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) ∧ 𝑋 = ∪ 𝑡) → (∃𝑓(𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈)) → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))) |
115 | 114 | expimpd 627 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ (𝒫 𝑅 ∩ Fin)) → ((𝑋 = ∪ 𝑡 ∧ ∃𝑓(𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈))) → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))) |
116 | 115 | rexlimdva 3013 |
. 2
⊢ (𝜑 → (∃𝑡 ∈ (𝒫 𝑅 ∩ Fin)(𝑋 = ∪ 𝑡 ∧ ∃𝑓(𝑓:𝑡⟶𝑆 ∧ ∀𝑢 ∈ 𝑡 (𝐴 ∈ (𝑓‘𝑢) ∧ (𝑢 × (𝑓‘𝑢)) ⊆ 𝑈))) → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈))) |
117 | 38, 116 | mpd 15 |
1
⊢ (𝜑 → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)) |