Step | Hyp | Ref
| Expression |
1 | | txcmp.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ Comp) |
2 | | txcmp.x |
. . . . 5
⊢ 𝑋 = ∪
𝑅 |
3 | | txcmp.y |
. . . . 5
⊢ 𝑌 = ∪
𝑆 |
4 | | txcmp.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Comp) |
5 | 4 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑅 ∈ Comp) |
6 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑆 ∈ Comp) |
7 | | txcmp.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ⊆ (𝑅 ×t 𝑆)) |
8 | 7 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑊 ⊆ (𝑅 ×t 𝑆)) |
9 | | txcmp.u |
. . . . . 6
⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝑊) |
10 | 9 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑋 × 𝑌) = ∪ 𝑊) |
11 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑌) |
12 | 2, 3, 5, 6, 8, 10,
11 | txcmplem1 21444 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑢) ⊆ ∪ 𝑣)) |
13 | 12 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑌 ∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑢) ⊆ ∪ 𝑣)) |
14 | | unieq 4444 |
. . . . 5
⊢ (𝑣 = (𝑓‘𝑢) → ∪ 𝑣 = ∪
(𝑓‘𝑢)) |
15 | 14 | sseq2d 3633 |
. . . 4
⊢ (𝑣 = (𝑓‘𝑢) → ((𝑋 × 𝑢) ⊆ ∪ 𝑣 ↔ (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢))) |
16 | 3, 15 | cmpcovf 21194 |
. . 3
⊢ ((𝑆 ∈ Comp ∧ ∀𝑥 ∈ 𝑌 ∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑢) ⊆ ∪ 𝑣)) → ∃𝑤 ∈ (𝒫 𝑆 ∩ Fin)(𝑌 = ∪ 𝑤 ∧ ∃𝑓(𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) |
17 | 1, 13, 16 | syl2anc 693 |
. 2
⊢ (𝜑 → ∃𝑤 ∈ (𝒫 𝑆 ∩ Fin)(𝑌 = ∪ 𝑤 ∧ ∃𝑓(𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) |
18 | | simprrl 804 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → 𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin)) |
19 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) → 𝑓 Fn 𝑤) |
20 | | fniunfv 6505 |
. . . . . . . . . . 11
⊢ (𝑓 Fn 𝑤 → ∪
𝑧 ∈ 𝑤 (𝑓‘𝑧) = ∪ ran 𝑓) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) = ∪ ran 𝑓) |
22 | | frn 6053 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝑊 ∩ Fin)) |
23 | 18, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ran 𝑓 ⊆ (𝒫 𝑊 ∩ Fin)) |
24 | | inss1 3833 |
. . . . . . . . . . . 12
⊢
(𝒫 𝑊 ∩
Fin) ⊆ 𝒫 𝑊 |
25 | 23, 24 | syl6ss 3615 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ran 𝑓 ⊆ 𝒫 𝑊) |
26 | | sspwuni 4611 |
. . . . . . . . . . 11
⊢ (ran
𝑓 ⊆ 𝒫 𝑊 ↔ ∪ ran 𝑓 ⊆ 𝑊) |
27 | 25, 26 | sylib 208 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∪ ran
𝑓 ⊆ 𝑊) |
28 | 21, 27 | eqsstrd 3639 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) ⊆ 𝑊) |
29 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
30 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝑓‘𝑧) ∈ V |
31 | 29, 30 | iunex 7147 |
. . . . . . . . . 10
⊢ ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) ∈ V |
32 | 31 | elpw 4164 |
. . . . . . . . 9
⊢ (∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) ∈ 𝒫 𝑊 ↔ ∪
𝑧 ∈ 𝑤 (𝑓‘𝑧) ⊆ 𝑊) |
33 | 28, 32 | sylibr 224 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) ∈ 𝒫 𝑊) |
34 | | inss2 3834 |
. . . . . . . . . 10
⊢
(𝒫 𝑆 ∩
Fin) ⊆ Fin |
35 | | simplr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) |
36 | 34, 35 | sseldi 3601 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → 𝑤 ∈ Fin) |
37 | | inss2 3834 |
. . . . . . . . . . 11
⊢
(𝒫 𝑊 ∩
Fin) ⊆ Fin |
38 | | fss 6056 |
. . . . . . . . . . 11
⊢ ((𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ (𝒫 𝑊 ∩ Fin) ⊆ Fin) →
𝑓:𝑤⟶Fin) |
39 | 18, 37, 38 | sylancl 694 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → 𝑓:𝑤⟶Fin) |
40 | | ffvelrn 6357 |
. . . . . . . . . . 11
⊢ ((𝑓:𝑤⟶Fin ∧ 𝑧 ∈ 𝑤) → (𝑓‘𝑧) ∈ Fin) |
41 | 40 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (𝑓:𝑤⟶Fin → ∀𝑧 ∈ 𝑤 (𝑓‘𝑧) ∈ Fin) |
42 | 39, 41 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∀𝑧 ∈ 𝑤 (𝑓‘𝑧) ∈ Fin) |
43 | | iunfi 8254 |
. . . . . . . . 9
⊢ ((𝑤 ∈ Fin ∧ ∀𝑧 ∈ 𝑤 (𝑓‘𝑧) ∈ Fin) → ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) ∈ Fin) |
44 | 36, 42, 43 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) ∈ Fin) |
45 | 33, 44 | elind 3798 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) ∈ (𝒫 𝑊 ∩ Fin)) |
46 | | simprl 794 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → 𝑌 = ∪ 𝑤) |
47 | | uniiun 4573 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑤 =
∪ 𝑧 ∈ 𝑤 𝑧 |
48 | 46, 47 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → 𝑌 = ∪ 𝑧 ∈ 𝑤 𝑧) |
49 | 48 | xpeq2d 5139 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → (𝑋 × 𝑌) = (𝑋 × ∪
𝑧 ∈ 𝑤 𝑧)) |
50 | | xpiundi 5173 |
. . . . . . . . . . 11
⊢ (𝑋 × ∪ 𝑧 ∈ 𝑤 𝑧) = ∪ 𝑧 ∈ 𝑤 (𝑋 × 𝑧) |
51 | 49, 50 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → (𝑋 × 𝑌) = ∪
𝑧 ∈ 𝑤 (𝑋 × 𝑧)) |
52 | | simprrr 805 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)) |
53 | | xpeq2 5129 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑧 → (𝑋 × 𝑢) = (𝑋 × 𝑧)) |
54 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑧 → (𝑓‘𝑢) = (𝑓‘𝑧)) |
55 | 54 | unieqd 4446 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑧 → ∪ (𝑓‘𝑢) = ∪ (𝑓‘𝑧)) |
56 | 53, 55 | sseq12d 3634 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑧 → ((𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢) ↔ (𝑋 × 𝑧) ⊆ ∪ (𝑓‘𝑧))) |
57 | 56 | cbvralv 3171 |
. . . . . . . . . . . 12
⊢
(∀𝑢 ∈
𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢) ↔ ∀𝑧 ∈ 𝑤 (𝑋 × 𝑧) ⊆ ∪ (𝑓‘𝑧)) |
58 | 52, 57 | sylib 208 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∀𝑧 ∈ 𝑤 (𝑋 × 𝑧) ⊆ ∪ (𝑓‘𝑧)) |
59 | | ss2iun 4536 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝑤 (𝑋 × 𝑧) ⊆ ∪ (𝑓‘𝑧) → ∪
𝑧 ∈ 𝑤 (𝑋 × 𝑧) ⊆ ∪
𝑧 ∈ 𝑤 ∪ (𝑓‘𝑧)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∪ 𝑧 ∈ 𝑤 (𝑋 × 𝑧) ⊆ ∪
𝑧 ∈ 𝑤 ∪ (𝑓‘𝑧)) |
61 | 51, 60 | eqsstrd 3639 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → (𝑋 × 𝑌) ⊆ ∪ 𝑧 ∈ 𝑤 ∪ (𝑓‘𝑧)) |
62 | 18 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) ∧ 𝑧 ∈ 𝑤) → (𝑓‘𝑧) ∈ (𝒫 𝑊 ∩ Fin)) |
63 | 24, 62 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) ∧ 𝑧 ∈ 𝑤) → (𝑓‘𝑧) ∈ 𝒫 𝑊) |
64 | | elpwi 4168 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑧) ∈ 𝒫 𝑊 → (𝑓‘𝑧) ⊆ 𝑊) |
65 | | uniss 4458 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑧) ⊆ 𝑊 → ∪ (𝑓‘𝑧) ⊆ ∪ 𝑊) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) ∧ 𝑧 ∈ 𝑤) → ∪ (𝑓‘𝑧) ⊆ ∪ 𝑊) |
67 | 9 | ad3antrrr 766 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) ∧ 𝑧 ∈ 𝑤) → (𝑋 × 𝑌) = ∪ 𝑊) |
68 | 66, 67 | sseqtr4d 3642 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) ∧ 𝑧 ∈ 𝑤) → ∪ (𝑓‘𝑧) ⊆ (𝑋 × 𝑌)) |
69 | 68 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∀𝑧 ∈ 𝑤 ∪ (𝑓‘𝑧) ⊆ (𝑋 × 𝑌)) |
70 | | iunss 4561 |
. . . . . . . . . 10
⊢ (∪ 𝑧 ∈ 𝑤 ∪ (𝑓‘𝑧) ⊆ (𝑋 × 𝑌) ↔ ∀𝑧 ∈ 𝑤 ∪ (𝑓‘𝑧) ⊆ (𝑋 × 𝑌)) |
71 | 69, 70 | sylibr 224 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∪ 𝑧 ∈ 𝑤 ∪ (𝑓‘𝑧) ⊆ (𝑋 × 𝑌)) |
72 | 61, 71 | eqssd 3620 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → (𝑋 × 𝑌) = ∪
𝑧 ∈ 𝑤 ∪ (𝑓‘𝑧)) |
73 | | iuncom4 4528 |
. . . . . . . 8
⊢ ∪ 𝑧 ∈ 𝑤 ∪ (𝑓‘𝑧) = ∪ ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) |
74 | 72, 73 | syl6eq 2672 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → (𝑋 × 𝑌) = ∪ ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧)) |
75 | | unieq 4444 |
. . . . . . . . 9
⊢ (𝑣 = ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) → ∪ 𝑣 = ∪
∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧)) |
76 | 75 | eqeq2d 2632 |
. . . . . . . 8
⊢ (𝑣 = ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) → ((𝑋 × 𝑌) = ∪ 𝑣 ↔ (𝑋 × 𝑌) = ∪ ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧))) |
77 | 76 | rspcev 3309 |
. . . . . . 7
⊢
((∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧) ∈ (𝒫 𝑊 ∩ Fin) ∧ (𝑋 × 𝑌) = ∪ ∪ 𝑧 ∈ 𝑤 (𝑓‘𝑧)) → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣) |
78 | 45, 74, 77 | syl2anc 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ (𝑌 = ∪ 𝑤 ∧ (𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)))) → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣) |
79 | 78 | expr 643 |
. . . . 5
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ 𝑌 = ∪ 𝑤) → ((𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)) → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣)) |
80 | 79 | exlimdv 1861 |
. . . 4
⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) ∧ 𝑌 = ∪ 𝑤) → (∃𝑓(𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢)) → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣)) |
81 | 80 | expimpd 629 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 𝑆 ∩ Fin)) → ((𝑌 = ∪ 𝑤 ∧ ∃𝑓(𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢))) → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣)) |
82 | 81 | rexlimdva 3031 |
. 2
⊢ (𝜑 → (∃𝑤 ∈ (𝒫 𝑆 ∩ Fin)(𝑌 = ∪ 𝑤 ∧ ∃𝑓(𝑓:𝑤⟶(𝒫 𝑊 ∩ Fin) ∧ ∀𝑢 ∈ 𝑤 (𝑋 × 𝑢) ⊆ ∪ (𝑓‘𝑢))) → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣)) |
83 | 17, 82 | mpd 15 |
1
⊢ (𝜑 → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣) |