Proof of Theorem supnfcls
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | disjdif 4471 | . 2
⊢ (𝑈 ∩ (𝑋 ∖ 𝑈)) = ∅ | 
| 2 |  | simpr 484 | . . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) ∧ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) → 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) | 
| 3 |  | simpl2 1192 | . . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) ∧ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) → 𝑈 ∈ 𝐽) | 
| 4 |  | simpl3 1193 | . . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) ∧ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) → 𝐴 ∈ 𝑈) | 
| 5 |  | sseq2 4009 | . . . . . 6
⊢ (𝑥 = (𝑋 ∖ 𝑈) → ((𝑋 ∖ 𝑈) ⊆ 𝑥 ↔ (𝑋 ∖ 𝑈) ⊆ (𝑋 ∖ 𝑈))) | 
| 6 |  | difss 4135 | . . . . . . 7
⊢ (𝑋 ∖ 𝑈) ⊆ 𝑋 | 
| 7 |  | simpl1 1191 | . . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) ∧ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) → 𝐽 ∈ (TopOn‘𝑋)) | 
| 8 |  | toponmax 22933 | . . . . . . . 8
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) | 
| 9 |  | elpw2g 5332 | . . . . . . . 8
⊢ (𝑋 ∈ 𝐽 → ((𝑋 ∖ 𝑈) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑈) ⊆ 𝑋)) | 
| 10 | 7, 8, 9 | 3syl 18 | . . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) ∧ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) → ((𝑋 ∖ 𝑈) ∈ 𝒫 𝑋 ↔ (𝑋 ∖ 𝑈) ⊆ 𝑋)) | 
| 11 | 6, 10 | mpbiri 258 | . . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) ∧ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) → (𝑋 ∖ 𝑈) ∈ 𝒫 𝑋) | 
| 12 |  | ssidd 4006 | . . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) ∧ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) → (𝑋 ∖ 𝑈) ⊆ (𝑋 ∖ 𝑈)) | 
| 13 | 5, 11, 12 | elrabd 3693 | . . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) ∧ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) → (𝑋 ∖ 𝑈) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥}) | 
| 14 |  | fclsopni 24024 | . . . . 5
⊢ ((𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥}) ∧ (𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈 ∧ (𝑋 ∖ 𝑈) ∈ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) → (𝑈 ∩ (𝑋 ∖ 𝑈)) ≠ ∅) | 
| 15 | 2, 3, 4, 13, 14 | syl13anc 1373 | . . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) ∧ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) → (𝑈 ∩ (𝑋 ∖ 𝑈)) ≠ ∅) | 
| 16 | 15 | ex 412 | . . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) → (𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥}) → (𝑈 ∩ (𝑋 ∖ 𝑈)) ≠ ∅)) | 
| 17 | 16 | necon2bd 2955 | . 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) → ((𝑈 ∩ (𝑋 ∖ 𝑈)) = ∅ → ¬ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥}))) | 
| 18 | 1, 17 | mpi 20 | 1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) → ¬ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) |