Step | Hyp | Ref
| Expression |
1 | | ssrab2 3650 |
. . . 4
⊢ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ⊆
𝒫 𝑋 |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ⊆ 𝒫 𝑋) |
3 | | inss1 3795 |
. . . . . 6
⊢ (𝑋 ∩ ∩ 𝑡)
⊆ 𝑋 |
4 | | elpw2g 4754 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → ((𝑋 ∩ ∩ 𝑡) ∈ 𝒫 𝑋 ↔ (𝑋 ∩ ∩ 𝑡) ⊆ 𝑋)) |
5 | 3, 4 | mpbiri 247 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∩ ∩ 𝑡) ∈ 𝒫 𝑋) |
6 | 5 | ad2antrr 758 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → (𝑋 ∩ ∩ 𝑡) ∈ 𝒫 𝑋) |
7 | | imassrn 5396 |
. . . . . . . . 9
⊢ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ ran 𝐹 |
8 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝐹:𝒫 𝑋⟶𝒫 𝑋 → ran 𝐹 ⊆ 𝒫 𝑋) |
9 | 8 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ran 𝐹 ⊆ 𝒫 𝑋) |
10 | 7, 9 | syl5ss 3579 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ 𝒫
𝑋) |
11 | 10 | unissd 4398 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ ∪ 𝒫 𝑋) |
12 | | unipw 4845 |
. . . . . . 7
⊢ ∪ 𝒫 𝑋 = 𝑋 |
13 | 11, 12 | syl6sseq 3614 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ 𝑋) |
14 | 13 | adantr 480 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ 𝑋) |
15 | | inss2 3796 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∩ ∩ 𝑡)
⊆ ∩ 𝑡 |
16 | | intss1 4427 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝑡 → ∩ 𝑡 ⊆ 𝑎) |
17 | 15, 16 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑡 → (𝑋 ∩ ∩ 𝑡) ⊆ 𝑎) |
18 | 17 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → (𝑋 ∩ ∩ 𝑡) ⊆ 𝑎) |
19 | | sspwb 4844 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∩ ∩ 𝑡)
⊆ 𝑎 ↔ 𝒫
(𝑋 ∩ ∩ 𝑡)
⊆ 𝒫 𝑎) |
20 | 18, 19 | sylib 207 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → 𝒫 (𝑋 ∩ ∩ 𝑡) ⊆ 𝒫 𝑎) |
21 | | ssrin 3800 |
. . . . . . . . . . 11
⊢
(𝒫 (𝑋 ∩
∩ 𝑡) ⊆ 𝒫 𝑎 → (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin) ⊆ (𝒫
𝑎 ∩
Fin)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin) ⊆ (𝒫
𝑎 ∩
Fin)) |
23 | | imass2 5420 |
. . . . . . . . . 10
⊢
((𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin) ⊆ (𝒫 𝑎 ∩ Fin) → (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ (𝐹
“ (𝒫 𝑎 ∩
Fin))) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ (𝐹 “ (𝒫 𝑎 ∩ Fin))) |
25 | 24 | unissd 4398 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin))) |
26 | | ssel2 3563 |
. . . . . . . . . 10
⊢ ((𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∧ 𝑎 ∈ 𝑡) → 𝑎 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) |
27 | | pweq 4111 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑎 → 𝒫 𝑠 = 𝒫 𝑎) |
28 | 27 | ineq1d 3775 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑎 → (𝒫 𝑠 ∩ Fin) = (𝒫 𝑎 ∩ Fin)) |
29 | 28 | imaeq2d 5385 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑎 → (𝐹 “ (𝒫 𝑠 ∩ Fin)) = (𝐹 “ (𝒫 𝑎 ∩ Fin))) |
30 | 29 | unieqd 4382 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑎 → ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) = ∪ (𝐹
“ (𝒫 𝑎 ∩
Fin))) |
31 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑎 → 𝑠 = 𝑎) |
32 | 30, 31 | sseq12d 3597 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑎 → (∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠 ↔ ∪ (𝐹
“ (𝒫 𝑎 ∩
Fin)) ⊆ 𝑎)) |
33 | 32 | elrab 3331 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ (𝑎 ∈ 𝒫 𝑋 ∧ ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎)) |
34 | 33 | simprbi 479 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} → ∪ (𝐹
“ (𝒫 𝑎 ∩
Fin)) ⊆ 𝑎) |
35 | 26, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎) |
36 | 35 | adantll 746 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎) |
37 | 25, 36 | sstrd 3578 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ 𝑎) |
38 | 37 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∀𝑎 ∈ 𝑡 ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ 𝑎) |
39 | | ssint 4428 |
. . . . . 6
⊢ (∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ ∩ 𝑡
↔ ∀𝑎 ∈
𝑡 ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ 𝑎) |
40 | 38, 39 | sylibr 223 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ ∩ 𝑡) |
41 | 14, 40 | ssind 3799 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ (𝑋 ∩ ∩ 𝑡)) |
42 | | pweq 4111 |
. . . . . . . . 9
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → 𝒫 𝑠 = 𝒫 (𝑋 ∩ ∩ 𝑡)) |
43 | 42 | ineq1d 3775 |
. . . . . . . 8
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → (𝒫 𝑠 ∩ Fin) = (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) |
44 | 43 | imaeq2d 5385 |
. . . . . . 7
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → (𝐹 “ (𝒫 𝑠 ∩ Fin)) = (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin))) |
45 | 44 | unieqd 4382 |
. . . . . 6
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) = ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin))) |
46 | | id 22 |
. . . . . 6
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → 𝑠 = (𝑋 ∩ ∩ 𝑡)) |
47 | 45, 46 | sseq12d 3597 |
. . . . 5
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → (∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠 ↔
∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ (𝑋 ∩ ∩ 𝑡))) |
48 | 47 | elrab 3331 |
. . . 4
⊢ ((𝑋 ∩ ∩ 𝑡)
∈ {𝑠 ∈ 𝒫
𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ↔
((𝑋 ∩ ∩ 𝑡)
∈ 𝒫 𝑋 ∧
∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ (𝑋 ∩ ∩ 𝑡))) |
49 | 6, 41, 48 | sylanbrc 695 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → (𝑋 ∩ ∩ 𝑡) ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) |
50 | 2, 49 | ismred2 16086 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (Moore‘𝑋)) |
51 | | fssxp 5973 |
. . . 4
⊢ (𝐹:𝒫 𝑋⟶𝒫 𝑋 → 𝐹 ⊆ (𝒫 𝑋 × 𝒫 𝑋)) |
52 | | pwexg 4776 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V) |
53 | | xpexg 6858 |
. . . . 5
⊢
((𝒫 𝑋 ∈
V ∧ 𝒫 𝑋 ∈
V) → (𝒫 𝑋
× 𝒫 𝑋) ∈
V) |
54 | 52, 52, 53 | syl2anc 691 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (𝒫 𝑋 × 𝒫 𝑋) ∈ V) |
55 | | ssexg 4732 |
. . . 4
⊢ ((𝐹 ⊆ (𝒫 𝑋 × 𝒫 𝑋) ∧ (𝒫 𝑋 × 𝒫 𝑋) ∈ V) → 𝐹 ∈ V) |
56 | 51, 54, 55 | syl2anr 494 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → 𝐹 ∈ V) |
57 | | simpr 476 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → 𝐹:𝒫 𝑋⟶𝒫 𝑋) |
58 | | pweq 4111 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → 𝒫 𝑠 = 𝒫 𝑡) |
59 | 58 | ineq1d 3775 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → (𝒫 𝑠 ∩ Fin) = (𝒫 𝑡 ∩ Fin)) |
60 | 59 | imaeq2d 5385 |
. . . . . . . 8
⊢ (𝑠 = 𝑡 → (𝐹 “ (𝒫 𝑠 ∩ Fin)) = (𝐹 “ (𝒫 𝑡 ∩ Fin))) |
61 | 60 | unieqd 4382 |
. . . . . . 7
⊢ (𝑠 = 𝑡 → ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) = ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin))) |
62 | | id 22 |
. . . . . . 7
⊢ (𝑠 = 𝑡 → 𝑠 = 𝑡) |
63 | 61, 62 | sseq12d 3597 |
. . . . . 6
⊢ (𝑠 = 𝑡 → (∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠 ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) |
64 | 63 | elrab3 3332 |
. . . . 5
⊢ (𝑡 ∈ 𝒫 𝑋 → (𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) |
65 | 64 | rgen 2906 |
. . . 4
⊢
∀𝑡 ∈
𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡) |
66 | 57, 65 | jctir 559 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → (𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡))) |
67 | | feq1 5939 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑓:𝒫 𝑋⟶𝒫 𝑋 ↔ 𝐹:𝒫 𝑋⟶𝒫 𝑋)) |
68 | | imaeq1 5380 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓 “ (𝒫 𝑡 ∩ Fin)) = (𝐹 “ (𝒫 𝑡 ∩ Fin))) |
69 | 68 | unieqd 4382 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ∪ (𝑓 “ (𝒫 𝑡 ∩ Fin)) = ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin))) |
70 | 69 | sseq1d 3595 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (∪ (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡 ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) |
71 | 70 | bibi2d 331 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡) ↔
(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ↔
∪ (𝐹 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))) |
72 | 71 | ralbidv 2969 |
. . . . 5
⊢ (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡) ↔
∀𝑡 ∈ 𝒫
𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡))) |
73 | 67, 72 | anbi12d 743 |
. . . 4
⊢ (𝑓 = 𝐹 → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) ↔
(𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)))) |
74 | 73 | spcegv 3267 |
. . 3
⊢ (𝐹 ∈ V → ((𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) →
∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)))) |
75 | 56, 66, 74 | sylc 63 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡))) |
76 | | isacs 16135 |
. 2
⊢ ({𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ∈
(ACS‘𝑋) ↔
({𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ∈
(Moore‘𝑋) ∧
∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)))) |
77 | 50, 75, 76 | sylanbrc 695 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (ACS‘𝑋)) |