Step | Hyp | Ref
| Expression |
1 | | ssrab2 3914 |
. . . 4
⊢ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ⊆
𝒫 𝑋 |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ⊆ 𝒫 𝑋) |
3 | | inss1 4059 |
. . . . . 6
⊢ (𝑋 ∩ ∩ 𝑡)
⊆ 𝑋 |
4 | | elpw2g 5051 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → ((𝑋 ∩ ∩ 𝑡) ∈ 𝒫 𝑋 ↔ (𝑋 ∩ ∩ 𝑡) ⊆ 𝑋)) |
5 | 3, 4 | mpbiri 250 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∩ ∩ 𝑡) ∈ 𝒫 𝑋) |
6 | 5 | ad2antrr 717 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → (𝑋 ∩ ∩ 𝑡) ∈ 𝒫 𝑋) |
7 | | imassrn 5722 |
. . . . . . . . 9
⊢ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ ran 𝐹 |
8 | | frn 6288 |
. . . . . . . . . 10
⊢ (𝐹:𝒫 𝑋⟶𝒫 𝑋 → ran 𝐹 ⊆ 𝒫 𝑋) |
9 | 8 | adantl 475 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ran 𝐹 ⊆ 𝒫 𝑋) |
10 | 7, 9 | syl5ss 3838 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ 𝒫
𝑋) |
11 | 10 | unissd 4686 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ ∪ 𝒫 𝑋) |
12 | | unipw 5141 |
. . . . . . 7
⊢ ∪ 𝒫 𝑋 = 𝑋 |
13 | 11, 12 | syl6sseq 3876 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ 𝑋) |
14 | 13 | adantr 474 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ 𝑋) |
15 | | inss2 4060 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∩ ∩ 𝑡)
⊆ ∩ 𝑡 |
16 | | intss1 4714 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝑡 → ∩ 𝑡 ⊆ 𝑎) |
17 | 15, 16 | syl5ss 3838 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑡 → (𝑋 ∩ ∩ 𝑡) ⊆ 𝑎) |
18 | 17 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → (𝑋 ∩ ∩ 𝑡) ⊆ 𝑎) |
19 | | sspwb 5140 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∩ ∩ 𝑡)
⊆ 𝑎 ↔ 𝒫
(𝑋 ∩ ∩ 𝑡)
⊆ 𝒫 𝑎) |
20 | 18, 19 | sylib 210 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → 𝒫 (𝑋 ∩ ∩ 𝑡) ⊆ 𝒫 𝑎) |
21 | 20 | ssrind 4066 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin) ⊆ (𝒫
𝑎 ∩
Fin)) |
22 | | imass2 5746 |
. . . . . . . . . 10
⊢
((𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin) ⊆ (𝒫 𝑎 ∩ Fin) → (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ (𝐹
“ (𝒫 𝑎 ∩
Fin))) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ (𝐹 “ (𝒫 𝑎 ∩ Fin))) |
24 | 23 | unissd 4686 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin))) |
25 | | ssel2 3822 |
. . . . . . . . . 10
⊢ ((𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∧ 𝑎 ∈ 𝑡) → 𝑎 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) |
26 | | pweq 4383 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑎 → 𝒫 𝑠 = 𝒫 𝑎) |
27 | 26 | ineq1d 4042 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑎 → (𝒫 𝑠 ∩ Fin) = (𝒫 𝑎 ∩ Fin)) |
28 | 27 | imaeq2d 5711 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑎 → (𝐹 “ (𝒫 𝑠 ∩ Fin)) = (𝐹 “ (𝒫 𝑎 ∩ Fin))) |
29 | 28 | unieqd 4670 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑎 → ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) = ∪ (𝐹
“ (𝒫 𝑎 ∩
Fin))) |
30 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑎 → 𝑠 = 𝑎) |
31 | 29, 30 | sseq12d 3859 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑎 → (∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠 ↔ ∪ (𝐹
“ (𝒫 𝑎 ∩
Fin)) ⊆ 𝑎)) |
32 | 31 | elrab 3585 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ (𝑎 ∈ 𝒫 𝑋 ∧ ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎)) |
33 | 32 | simprbi 492 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} → ∪ (𝐹
“ (𝒫 𝑎 ∩
Fin)) ⊆ 𝑎) |
34 | 25, 33 | syl 17 |
. . . . . . . . 9
⊢ ((𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎) |
35 | 34 | adantll 705 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎) |
36 | 24, 35 | sstrd 3837 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ 𝑎) |
37 | 36 | ralrimiva 3175 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∀𝑎 ∈ 𝑡 ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ 𝑎) |
38 | | ssint 4715 |
. . . . . 6
⊢ (∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ ∩ 𝑡
↔ ∀𝑎 ∈
𝑡 ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ 𝑎) |
39 | 37, 38 | sylibr 226 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ ∩ 𝑡) |
40 | 14, 39 | ssind 4063 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ (𝑋 ∩ ∩ 𝑡)) |
41 | | pweq 4383 |
. . . . . . . . 9
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → 𝒫 𝑠 = 𝒫 (𝑋 ∩ ∩ 𝑡)) |
42 | 41 | ineq1d 4042 |
. . . . . . . 8
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → (𝒫 𝑠 ∩ Fin) = (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) |
43 | 42 | imaeq2d 5711 |
. . . . . . 7
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → (𝐹 “ (𝒫 𝑠 ∩ Fin)) = (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin))) |
44 | 43 | unieqd 4670 |
. . . . . 6
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) = ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin))) |
45 | | id 22 |
. . . . . 6
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → 𝑠 = (𝑋 ∩ ∩ 𝑡)) |
46 | 44, 45 | sseq12d 3859 |
. . . . 5
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → (∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠 ↔
∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ (𝑋 ∩ ∩ 𝑡))) |
47 | 46 | elrab 3585 |
. . . 4
⊢ ((𝑋 ∩ ∩ 𝑡)
∈ {𝑠 ∈ 𝒫
𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ↔
((𝑋 ∩ ∩ 𝑡)
∈ 𝒫 𝑋 ∧
∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ (𝑋 ∩ ∩ 𝑡))) |
48 | 6, 40, 47 | sylanbrc 578 |
. . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → (𝑋 ∩ ∩ 𝑡) ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) |
49 | 2, 48 | ismred2 16623 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (Moore‘𝑋)) |
50 | | fssxp 6301 |
. . . 4
⊢ (𝐹:𝒫 𝑋⟶𝒫 𝑋 → 𝐹 ⊆ (𝒫 𝑋 × 𝒫 𝑋)) |
51 | | pwexg 5080 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V) |
52 | 51, 51 | xpexd 7226 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (𝒫 𝑋 × 𝒫 𝑋) ∈ V) |
53 | | ssexg 5031 |
. . . 4
⊢ ((𝐹 ⊆ (𝒫 𝑋 × 𝒫 𝑋) ∧ (𝒫 𝑋 × 𝒫 𝑋) ∈ V) → 𝐹 ∈ V) |
54 | 50, 52, 53 | syl2anr 590 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → 𝐹 ∈ V) |
55 | | simpr 479 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → 𝐹:𝒫 𝑋⟶𝒫 𝑋) |
56 | | pweq 4383 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑡 → 𝒫 𝑠 = 𝒫 𝑡) |
57 | 56 | ineq1d 4042 |
. . . . . . . . 9
⊢ (𝑠 = 𝑡 → (𝒫 𝑠 ∩ Fin) = (𝒫 𝑡 ∩ Fin)) |
58 | 57 | imaeq2d 5711 |
. . . . . . . 8
⊢ (𝑠 = 𝑡 → (𝐹 “ (𝒫 𝑠 ∩ Fin)) = (𝐹 “ (𝒫 𝑡 ∩ Fin))) |
59 | 58 | unieqd 4670 |
. . . . . . 7
⊢ (𝑠 = 𝑡 → ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) = ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin))) |
60 | | id 22 |
. . . . . . 7
⊢ (𝑠 = 𝑡 → 𝑠 = 𝑡) |
61 | 59, 60 | sseq12d 3859 |
. . . . . 6
⊢ (𝑠 = 𝑡 → (∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠 ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) |
62 | 61 | elrab3 3587 |
. . . . 5
⊢ (𝑡 ∈ 𝒫 𝑋 → (𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) |
63 | 62 | rgen 3131 |
. . . 4
⊢
∀𝑡 ∈
𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡) |
64 | 55, 63 | jctir 516 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → (𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡))) |
65 | | feq1 6263 |
. . . . 5
⊢ (𝑓 = 𝐹 → (𝑓:𝒫 𝑋⟶𝒫 𝑋 ↔ 𝐹:𝒫 𝑋⟶𝒫 𝑋)) |
66 | | imaeq1 5706 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓 “ (𝒫 𝑡 ∩ Fin)) = (𝐹 “ (𝒫 𝑡 ∩ Fin))) |
67 | 66 | unieqd 4670 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ∪ (𝑓 “ (𝒫 𝑡 ∩ Fin)) = ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin))) |
68 | 67 | sseq1d 3857 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (∪ (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡 ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) |
69 | 68 | bibi2d 334 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡) ↔
(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ↔
∪ (𝐹 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))) |
70 | 69 | ralbidv 3195 |
. . . . 5
⊢ (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡) ↔
∀𝑡 ∈ 𝒫
𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡))) |
71 | 65, 70 | anbi12d 624 |
. . . 4
⊢ (𝑓 = 𝐹 → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) ↔
(𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)))) |
72 | 71 | spcegv 3511 |
. . 3
⊢ (𝐹 ∈ V → ((𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) →
∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)))) |
73 | 54, 64, 72 | sylc 65 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡))) |
74 | | isacs 16671 |
. 2
⊢ ({𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ∈
(ACS‘𝑋) ↔
({𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ∈
(Moore‘𝑋) ∧
∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)))) |
75 | 49, 73, 74 | sylanbrc 578 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (ACS‘𝑋)) |