Step | Hyp | Ref
| Expression |
1 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) |
2 | | elin 3758 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝒫 𝑦 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑦 ∧ 𝑥 ∈ Fin)) |
3 | 1, 2 | sylib 207 |
. . . . . . . . . . . . . 14
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → (𝑥 ∈ 𝒫 𝑦 ∧ 𝑥 ∈ Fin)) |
4 | 3 | simpld 474 |
. . . . . . . . . . . . 13
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → 𝑥 ∈ 𝒫 𝑦) |
5 | | elpwi 4117 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝒫 𝑦 → 𝑥 ⊆ 𝑦) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → 𝑥 ⊆ 𝑦) |
7 | | elpwi 4117 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 𝑗 → 𝑦 ⊆ 𝑗) |
8 | 7 | ad4antlr 765 |
. . . . . . . . . . . 12
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → 𝑦 ⊆ 𝑗) |
9 | 6, 8 | sstrd 3578 |
. . . . . . . . . . 11
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → 𝑥 ⊆ 𝑗) |
10 | | selpw 4115 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑗 ↔ 𝑥 ⊆ 𝑗) |
11 | 9, 10 | sylibr 223 |
. . . . . . . . . 10
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → 𝑥 ∈ 𝒫 𝑗) |
12 | 3 | simprd 478 |
. . . . . . . . . 10
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → 𝑥 ∈ Fin) |
13 | 11, 12 | elind 3760 |
. . . . . . . . 9
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → 𝑥 ∈ (𝒫 𝑗 ∩ Fin)) |
14 | | simpr 476 |
. . . . . . . . . . 11
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → ∪ 𝑗 = ∪
𝑥) |
15 | | simpllr 795 |
. . . . . . . . . . 11
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → ∪ 𝑗 = ∪
𝑦) |
16 | 14, 15 | eqtr3d 2646 |
. . . . . . . . . 10
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → ∪ 𝑥 = ∪
𝑦) |
17 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝑥 =
∪ 𝑥 |
18 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝑦 =
∪ 𝑦 |
19 | 17, 18 | ssref 21125 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 𝑗 ∧ 𝑥 ⊆ 𝑦 ∧ ∪ 𝑥 = ∪
𝑦) → 𝑥Ref𝑦) |
20 | 11, 6, 16, 19 | syl3anc 1318 |
. . . . . . . . 9
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → 𝑥Ref𝑦) |
21 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑧Ref𝑦 ↔ 𝑥Ref𝑦)) |
22 | 21 | rspcev 3282 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝒫 𝑗 ∩ Fin) ∧ 𝑥Ref𝑦) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦) |
23 | 13, 20, 22 | syl2anc 691 |
. . . . . . . 8
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑥 ∈ (𝒫 𝑦 ∩ Fin)) ∧ ∪ 𝑗 =
∪ 𝑥) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦) |
24 | 23 | r19.29an 3059 |
. . . . . . 7
⊢ ((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑗 = ∪
𝑥) → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦) |
25 | | simplr 788 |
. . . . . . . . . 10
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) |
26 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
27 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑧 =
∪ 𝑧 |
28 | 27, 18 | isref 21122 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ V → (𝑧Ref𝑦 ↔ (∪ 𝑦 = ∪
𝑧 ∧ ∀𝑢 ∈ 𝑧 ∃𝑣 ∈ 𝑦 𝑢 ⊆ 𝑣))) |
29 | 26, 28 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑧Ref𝑦 ↔ (∪ 𝑦 = ∪
𝑧 ∧ ∀𝑢 ∈ 𝑧 ∃𝑣 ∈ 𝑦 𝑢 ⊆ 𝑣)) |
30 | 29 | simprbi 479 |
. . . . . . . . . . 11
⊢ (𝑧Ref𝑦 → ∀𝑢 ∈ 𝑧 ∃𝑣 ∈ 𝑦 𝑢 ⊆ 𝑣) |
31 | 30 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∀𝑢 ∈ 𝑧 ∃𝑣 ∈ 𝑦 𝑢 ⊆ 𝑣) |
32 | | sseq2 3590 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑓‘𝑢) → (𝑢 ⊆ 𝑣 ↔ 𝑢 ⊆ (𝑓‘𝑢))) |
33 | 32 | ac6sg 9193 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝒫 𝑗 ∩ Fin) →
(∀𝑢 ∈ 𝑧 ∃𝑣 ∈ 𝑦 𝑢 ⊆ 𝑣 → ∃𝑓(𝑓:𝑧⟶𝑦 ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)))) |
34 | 25, 31, 33 | sylc 63 |
. . . . . . . . 9
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∃𝑓(𝑓:𝑧⟶𝑦 ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢))) |
35 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → 𝑓:𝑧⟶𝑦) |
36 | | frn 5966 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝑧⟶𝑦 → ran 𝑓 ⊆ 𝑦) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ran 𝑓 ⊆ 𝑦) |
38 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑓 ∈ V |
39 | 38 | rnex 6992 |
. . . . . . . . . . . . . . 15
⊢ ran 𝑓 ∈ V |
40 | 39 | elpw 4114 |
. . . . . . . . . . . . . 14
⊢ (ran
𝑓 ∈ 𝒫 𝑦 ↔ ran 𝑓 ⊆ 𝑦) |
41 | 37, 40 | sylibr 223 |
. . . . . . . . . . . . 13
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ran 𝑓 ∈ 𝒫 𝑦) |
42 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑧⟶𝑦 → 𝑓 Fn 𝑧) |
43 | 35, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → 𝑓 Fn 𝑧) |
44 | | elin 3758 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (𝒫 𝑗 ∩ Fin) ↔ (𝑧 ∈ 𝒫 𝑗 ∧ 𝑧 ∈ Fin)) |
45 | 44 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝒫 𝑗 ∩ Fin) → 𝑧 ∈ Fin) |
46 | 45 | ad4antlr 765 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → 𝑧 ∈ Fin) |
47 | | fnfi 8123 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 Fn 𝑧 ∧ 𝑧 ∈ Fin) → 𝑓 ∈ Fin) |
48 | 43, 46, 47 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → 𝑓 ∈ Fin) |
49 | | rnfi 8132 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ Fin → ran 𝑓 ∈ Fin) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ran 𝑓 ∈ Fin) |
51 | 41, 50 | elind 3760 |
. . . . . . . . . . . 12
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ran 𝑓 ∈ (𝒫 𝑦 ∩ Fin)) |
52 | | simp-5r 805 |
. . . . . . . . . . . . 13
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ∪ 𝑗 = ∪
𝑦) |
53 | 27, 18 | refbas 21123 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧Ref𝑦 → ∪ 𝑦 = ∪
𝑧) |
54 | 53 | ad3antlr 763 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ∪ 𝑦 = ∪
𝑧) |
55 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑢(((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) |
56 | | nfra1 2925 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑢∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢) |
57 | 55, 56 | nfan 1816 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑢((((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) |
58 | | rspa 2914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑢 ∈
𝑧 𝑢 ⊆ (𝑓‘𝑢) ∧ 𝑢 ∈ 𝑧) → 𝑢 ⊆ (𝑓‘𝑢)) |
59 | 58 | adantll 746 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) ∧ 𝑢 ∈ 𝑧) → 𝑢 ⊆ (𝑓‘𝑢)) |
60 | 59 | sseld 3567 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) ∧ 𝑢 ∈ 𝑧) → (𝑥 ∈ 𝑢 → 𝑥 ∈ (𝑓‘𝑢))) |
61 | 60 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → (𝑢 ∈ 𝑧 → (𝑥 ∈ 𝑢 → 𝑥 ∈ (𝑓‘𝑢)))) |
62 | 57, 61 | reximdai 2995 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → (∃𝑢 ∈ 𝑧 𝑥 ∈ 𝑢 → ∃𝑢 ∈ 𝑧 𝑥 ∈ (𝑓‘𝑢))) |
63 | | eluni2 4376 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ∪ 𝑧
↔ ∃𝑢 ∈
𝑧 𝑥 ∈ 𝑢) |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → (𝑥 ∈ ∪ 𝑧 ↔ ∃𝑢 ∈ 𝑧 𝑥 ∈ 𝑢)) |
65 | | fnunirn 6415 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 Fn 𝑧 → (𝑥 ∈ ∪ ran
𝑓 ↔ ∃𝑢 ∈ 𝑧 𝑥 ∈ (𝑓‘𝑢))) |
66 | 43, 65 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → (𝑥 ∈ ∪ ran
𝑓 ↔ ∃𝑢 ∈ 𝑧 𝑥 ∈ (𝑓‘𝑢))) |
67 | 62, 64, 66 | 3imtr4d 282 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → (𝑥 ∈ ∪ 𝑧 → 𝑥 ∈ ∪ ran
𝑓)) |
68 | 67 | ssrdv 3574 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ∪ 𝑧 ⊆ ∪ ran 𝑓) |
69 | 54, 68 | eqsstrd 3602 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ∪ 𝑦 ⊆ ∪ ran 𝑓) |
70 | 37 | unissd 4398 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ∪ ran
𝑓 ⊆ ∪ 𝑦) |
71 | 69, 70 | eqssd 3585 |
. . . . . . . . . . . . 13
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ∪ 𝑦 = ∪
ran 𝑓) |
72 | 52, 71 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ∪ 𝑗 = ∪
ran 𝑓) |
73 | | unieq 4380 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ran 𝑓 → ∪ 𝑥 = ∪
ran 𝑓) |
74 | 73 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ran 𝑓 → (∪ 𝑗 = ∪
𝑥 ↔ ∪ 𝑗 =
∪ ran 𝑓)) |
75 | 74 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ ((ran
𝑓 ∈ (𝒫 𝑦 ∩ Fin) ∧ ∪ 𝑗 =
∪ ran 𝑓) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑗 = ∪
𝑥) |
76 | 51, 72, 75 | syl2anc 691 |
. . . . . . . . . . 11
⊢
(((((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) ∧ 𝑓:𝑧⟶𝑦) ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑗 = ∪
𝑥) |
77 | 76 | expl 646 |
. . . . . . . . . 10
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ((𝑓:𝑧⟶𝑦 ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑗 = ∪
𝑥)) |
78 | 77 | exlimdv 1848 |
. . . . . . . . 9
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → (∃𝑓(𝑓:𝑧⟶𝑦 ∧ ∀𝑢 ∈ 𝑧 𝑢 ⊆ (𝑓‘𝑢)) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑗 = ∪
𝑥)) |
79 | 34, 78 | mpd 15 |
. . . . . . . 8
⊢
(((((𝑗 ∈ Top
∧ 𝑦 ∈ 𝒫
𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ 𝑧 ∈ (𝒫 𝑗 ∩ Fin)) ∧ 𝑧Ref𝑦) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑗 = ∪
𝑥) |
80 | 79 | r19.29an 3059 |
. . . . . . 7
⊢ ((((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) ∧ ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦) → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑗 = ∪
𝑥) |
81 | 24, 80 | impbida 873 |
. . . . . 6
⊢ (((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) ∧ ∪ 𝑗 =
∪ 𝑦) → (∃𝑥 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑗 = ∪
𝑥 ↔ ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦)) |
82 | 81 | pm5.74da 719 |
. . . . 5
⊢ ((𝑗 ∈ Top ∧ 𝑦 ∈ 𝒫 𝑗) → ((∪ 𝑗 =
∪ 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑗 = ∪
𝑥) ↔ (∪ 𝑗 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦))) |
83 | 82 | ralbidva 2968 |
. . . 4
⊢ (𝑗 ∈ Top →
(∀𝑦 ∈ 𝒫
𝑗(∪ 𝑗 =
∪ 𝑦 → ∃𝑥 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑗 = ∪
𝑥) ↔ ∀𝑦 ∈ 𝒫 𝑗(∪
𝑗 = ∪ 𝑦
→ ∃𝑧 ∈
(𝒫 𝑗 ∩
Fin)𝑧Ref𝑦))) |
84 | 83 | pm5.32i 667 |
. . 3
⊢ ((𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗(∪
𝑗 = ∪ 𝑦
→ ∃𝑥 ∈
(𝒫 𝑦 ∩
Fin)∪ 𝑗 = ∪ 𝑥)) ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗(∪ 𝑗 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦))) |
85 | | eqid 2610 |
. . . 4
⊢ ∪ 𝑗 =
∪ 𝑗 |
86 | 85 | iscmp 21001 |
. . 3
⊢ (𝑗 ∈ Comp ↔ (𝑗 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝑗(∪
𝑗 = ∪ 𝑦
→ ∃𝑥 ∈
(𝒫 𝑦 ∩
Fin)∪ 𝑗 = ∪ 𝑥))) |
87 | 85 | iscref 29239 |
. . 3
⊢ (𝑗 ∈ CovHasRefFin ↔
(𝑗 ∈ Top ∧
∀𝑦 ∈ 𝒫
𝑗(∪ 𝑗 =
∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ Fin)𝑧Ref𝑦))) |
88 | 84, 86, 87 | 3bitr4i 291 |
. 2
⊢ (𝑗 ∈ Comp ↔ 𝑗 ∈
CovHasRefFin) |
89 | 88 | eqriv 2607 |
1
⊢ Comp =
CovHasRefFin |