| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssrab2 4080 | . . . 4
⊢ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ⊆
𝒫 𝑋 | 
| 2 | 1 | a1i 11 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ⊆ 𝒫 𝑋) | 
| 3 |  | pweq 4614 | . . . . . . . 8
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → 𝒫 𝑠 = 𝒫 (𝑋 ∩ ∩ 𝑡)) | 
| 4 | 3 | ineq1d 4219 | . . . . . . 7
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → (𝒫 𝑠 ∩ Fin) = (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) | 
| 5 | 4 | imaeq2d 6078 | . . . . . 6
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → (𝐹 “ (𝒫 𝑠 ∩ Fin)) = (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin))) | 
| 6 | 5 | unieqd 4920 | . . . . 5
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) = ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin))) | 
| 7 |  | id 22 | . . . . 5
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → 𝑠 = (𝑋 ∩ ∩ 𝑡)) | 
| 8 | 6, 7 | sseq12d 4017 | . . . 4
⊢ (𝑠 = (𝑋 ∩ ∩ 𝑡) → (∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠 ↔
∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ (𝑋 ∩ ∩ 𝑡))) | 
| 9 |  | inss1 4237 | . . . . . 6
⊢ (𝑋 ∩ ∩ 𝑡)
⊆ 𝑋 | 
| 10 |  | elpw2g 5333 | . . . . . 6
⊢ (𝑋 ∈ 𝑉 → ((𝑋 ∩ ∩ 𝑡) ∈ 𝒫 𝑋 ↔ (𝑋 ∩ ∩ 𝑡) ⊆ 𝑋)) | 
| 11 | 9, 10 | mpbiri 258 | . . . . 5
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∩ ∩ 𝑡) ∈ 𝒫 𝑋) | 
| 12 | 11 | ad2antrr 726 | . . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → (𝑋 ∩ ∩ 𝑡) ∈ 𝒫 𝑋) | 
| 13 |  | imassrn 6089 | . . . . . . . . 9
⊢ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ ran 𝐹 | 
| 14 |  | frn 6743 | . . . . . . . . . 10
⊢ (𝐹:𝒫 𝑋⟶𝒫 𝑋 → ran 𝐹 ⊆ 𝒫 𝑋) | 
| 15 | 14 | adantl 481 | . . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ran 𝐹 ⊆ 𝒫 𝑋) | 
| 16 | 13, 15 | sstrid 3995 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ 𝒫
𝑋) | 
| 17 | 16 | unissd 4917 | . . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ ∪ 𝒫 𝑋) | 
| 18 |  | unipw 5455 | . . . . . . 7
⊢ ∪ 𝒫 𝑋 = 𝑋 | 
| 19 | 17, 18 | sseqtrdi 4024 | . . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ 𝑋) | 
| 20 | 19 | adantr 480 | . . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ 𝑋) | 
| 21 |  | inss2 4238 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∩ ∩ 𝑡)
⊆ ∩ 𝑡 | 
| 22 |  | intss1 4963 | . . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝑡 → ∩ 𝑡 ⊆ 𝑎) | 
| 23 | 21, 22 | sstrid 3995 | . . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑡 → (𝑋 ∩ ∩ 𝑡) ⊆ 𝑎) | 
| 24 | 23 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → (𝑋 ∩ ∩ 𝑡) ⊆ 𝑎) | 
| 25 | 24 | sspwd 4613 | . . . . . . . . . . 11
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → 𝒫 (𝑋 ∩ ∩ 𝑡) ⊆ 𝒫 𝑎) | 
| 26 | 25 | ssrind 4244 | . . . . . . . . . 10
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin) ⊆ (𝒫
𝑎 ∩
Fin)) | 
| 27 |  | imass2 6120 | . . . . . . . . . 10
⊢
((𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin) ⊆ (𝒫 𝑎 ∩ Fin) → (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ (𝐹
“ (𝒫 𝑎 ∩
Fin))) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . 9
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡) ∩ Fin)) ⊆ (𝐹 “ (𝒫 𝑎 ∩ Fin))) | 
| 29 | 28 | unissd 4917 | . . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin))) | 
| 30 |  | ssel2 3978 | . . . . . . . . . 10
⊢ ((𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∧ 𝑎 ∈ 𝑡) → 𝑎 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) | 
| 31 |  | pweq 4614 | . . . . . . . . . . . . . . . 16
⊢ (𝑠 = 𝑎 → 𝒫 𝑠 = 𝒫 𝑎) | 
| 32 | 31 | ineq1d 4219 | . . . . . . . . . . . . . . 15
⊢ (𝑠 = 𝑎 → (𝒫 𝑠 ∩ Fin) = (𝒫 𝑎 ∩ Fin)) | 
| 33 | 32 | imaeq2d 6078 | . . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑎 → (𝐹 “ (𝒫 𝑠 ∩ Fin)) = (𝐹 “ (𝒫 𝑎 ∩ Fin))) | 
| 34 | 33 | unieqd 4920 | . . . . . . . . . . . . 13
⊢ (𝑠 = 𝑎 → ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) = ∪ (𝐹
“ (𝒫 𝑎 ∩
Fin))) | 
| 35 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑠 = 𝑎 → 𝑠 = 𝑎) | 
| 36 | 34, 35 | sseq12d 4017 | . . . . . . . . . . . 12
⊢ (𝑠 = 𝑎 → (∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠 ↔ ∪ (𝐹
“ (𝒫 𝑎 ∩
Fin)) ⊆ 𝑎)) | 
| 37 | 36 | elrab 3692 | . . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ (𝑎 ∈ 𝒫 𝑋 ∧ ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎)) | 
| 38 | 37 | simprbi 496 | . . . . . . . . . 10
⊢ (𝑎 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} → ∪ (𝐹
“ (𝒫 𝑎 ∩
Fin)) ⊆ 𝑎) | 
| 39 | 30, 38 | syl 17 | . . . . . . . . 9
⊢ ((𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎) | 
| 40 | 39 | adantll 714 | . . . . . . . 8
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 𝑎 ∩ Fin)) ⊆ 𝑎) | 
| 41 | 29, 40 | sstrd 3994 | . . . . . . 7
⊢ ((((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) ∧ 𝑎 ∈ 𝑡) → ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ 𝑎) | 
| 42 | 41 | ralrimiva 3146 | . . . . . 6
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∀𝑎 ∈ 𝑡 ∪ (𝐹 “ (𝒫 (𝑋 ∩ ∩ 𝑡)
∩ Fin)) ⊆ 𝑎) | 
| 43 |  | ssint 4964 | . . . . . 6
⊢ (∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ ∩ 𝑡
↔ ∀𝑎 ∈
𝑡 ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ 𝑎) | 
| 44 | 42, 43 | sylibr 234 | . . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ ∩ 𝑡) | 
| 45 | 20, 44 | ssind 4241 | . . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → ∪ (𝐹
“ (𝒫 (𝑋 ∩
∩ 𝑡) ∩ Fin)) ⊆ (𝑋 ∩ ∩ 𝑡)) | 
| 46 | 8, 12, 45 | elrabd 3694 | . . 3
⊢ (((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) ∧ 𝑡 ⊆ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) → (𝑋 ∩ ∩ 𝑡) ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠}) | 
| 47 | 2, 46 | ismred2 17646 | . 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (Moore‘𝑋)) | 
| 48 |  | fssxp 6763 | . . . 4
⊢ (𝐹:𝒫 𝑋⟶𝒫 𝑋 → 𝐹 ⊆ (𝒫 𝑋 × 𝒫 𝑋)) | 
| 49 |  | pwexg 5378 | . . . . 5
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ V) | 
| 50 | 49, 49 | xpexd 7771 | . . . 4
⊢ (𝑋 ∈ 𝑉 → (𝒫 𝑋 × 𝒫 𝑋) ∈ V) | 
| 51 |  | ssexg 5323 | . . . 4
⊢ ((𝐹 ⊆ (𝒫 𝑋 × 𝒫 𝑋) ∧ (𝒫 𝑋 × 𝒫 𝑋) ∈ V) → 𝐹 ∈ V) | 
| 52 | 48, 50, 51 | syl2anr 597 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → 𝐹 ∈ V) | 
| 53 |  | simpr 484 | . . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → 𝐹:𝒫 𝑋⟶𝒫 𝑋) | 
| 54 |  | pweq 4614 | . . . . . . . . . 10
⊢ (𝑠 = 𝑡 → 𝒫 𝑠 = 𝒫 𝑡) | 
| 55 | 54 | ineq1d 4219 | . . . . . . . . 9
⊢ (𝑠 = 𝑡 → (𝒫 𝑠 ∩ Fin) = (𝒫 𝑡 ∩ Fin)) | 
| 56 | 55 | imaeq2d 6078 | . . . . . . . 8
⊢ (𝑠 = 𝑡 → (𝐹 “ (𝒫 𝑠 ∩ Fin)) = (𝐹 “ (𝒫 𝑡 ∩ Fin))) | 
| 57 | 56 | unieqd 4920 | . . . . . . 7
⊢ (𝑠 = 𝑡 → ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) = ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin))) | 
| 58 |  | id 22 | . . . . . . 7
⊢ (𝑠 = 𝑡 → 𝑠 = 𝑡) | 
| 59 | 57, 58 | sseq12d 4017 | . . . . . 6
⊢ (𝑠 = 𝑡 → (∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠 ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) | 
| 60 | 59 | elrab3 3693 | . . . . 5
⊢ (𝑡 ∈ 𝒫 𝑋 → (𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) | 
| 61 | 60 | rgen 3063 | . . . 4
⊢
∀𝑡 ∈
𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡) | 
| 62 | 53, 61 | jctir 520 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → (𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡))) | 
| 63 |  | feq1 6716 | . . . 4
⊢ (𝑓 = 𝐹 → (𝑓:𝒫 𝑋⟶𝒫 𝑋 ↔ 𝐹:𝒫 𝑋⟶𝒫 𝑋)) | 
| 64 |  | imaeq1 6073 | . . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓 “ (𝒫 𝑡 ∩ Fin)) = (𝐹 “ (𝒫 𝑡 ∩ Fin))) | 
| 65 | 64 | unieqd 4920 | . . . . . . 7
⊢ (𝑓 = 𝐹 → ∪ (𝑓 “ (𝒫 𝑡 ∩ Fin)) = ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin))) | 
| 66 | 65 | sseq1d 4015 | . . . . . 6
⊢ (𝑓 = 𝐹 → (∪ (𝑓 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡 ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) | 
| 67 | 66 | bibi2d 342 | . . . . 5
⊢ (𝑓 = 𝐹 → ((𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡) ↔
(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ↔
∪ (𝐹 “ (𝒫 𝑡 ∩ Fin)) ⊆ 𝑡))) | 
| 68 | 67 | ralbidv 3178 | . . . 4
⊢ (𝑓 = 𝐹 → (∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡) ↔
∀𝑡 ∈ 𝒫
𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡))) | 
| 69 | 63, 68 | anbi12d 632 | . . 3
⊢ (𝑓 = 𝐹 → ((𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)) ↔
(𝐹:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝐹
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)))) | 
| 70 | 52, 62, 69 | spcedv 3598 | . 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → ∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡))) | 
| 71 |  | isacs 17694 | . 2
⊢ ({𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ∈
(ACS‘𝑋) ↔
({𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹
“ (𝒫 𝑠 ∩
Fin)) ⊆ 𝑠} ∈
(Moore‘𝑋) ∧
∃𝑓(𝑓:𝒫 𝑋⟶𝒫 𝑋 ∧ ∀𝑡 ∈ 𝒫 𝑋(𝑡 ∈ {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ↔ ∪ (𝑓
“ (𝒫 𝑡 ∩
Fin)) ⊆ 𝑡)))) | 
| 72 | 47, 70, 71 | sylanbrc 583 | 1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹:𝒫 𝑋⟶𝒫 𝑋) → {𝑠 ∈ 𝒫 𝑋 ∣ ∪ (𝐹 “ (𝒫 𝑠 ∩ Fin)) ⊆ 𝑠} ∈ (ACS‘𝑋)) |