| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | anass 468 | . 2
⊢ ((((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)) ↔ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran
Fil) ∧ (𝑋 = ∪ 𝐹
∧ ∀𝑠 ∈
𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)))) | 
| 2 |  | fvssunirn 6939 | . . . . . . . 8
⊢
(Fil‘𝑋)
⊆ ∪ ran Fil | 
| 3 | 2 | sseli 3979 | . . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ ∪ ran
Fil) | 
| 4 |  | filunibas 23889 | . . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 =
𝑋) | 
| 5 | 4 | eqcomd 2743 | . . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 = ∪ 𝐹) | 
| 6 | 3, 5 | jca 511 | . . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ ∪ ran Fil
∧ 𝑋 = ∪ 𝐹)) | 
| 7 |  | filunirn 23890 | . . . . . . 7
⊢ (𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ (Fil‘∪ 𝐹)) | 
| 8 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑋 = ∪
𝐹 → (Fil‘𝑋) = (Fil‘∪ 𝐹)) | 
| 9 | 8 | eleq2d 2827 | . . . . . . . 8
⊢ (𝑋 = ∪
𝐹 → (𝐹 ∈ (Fil‘𝑋) ↔ 𝐹 ∈ (Fil‘∪ 𝐹))) | 
| 10 | 9 | biimparc 479 | . . . . . . 7
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑋 = ∪ 𝐹)
→ 𝐹 ∈
(Fil‘𝑋)) | 
| 11 | 7, 10 | sylanb 581 | . . . . . 6
⊢ ((𝐹 ∈ ∪ ran Fil ∧ 𝑋 = ∪ 𝐹) → 𝐹 ∈ (Fil‘𝑋)) | 
| 12 | 6, 11 | impbii 209 | . . . . 5
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ ∪ ran Fil
∧ 𝑋 = ∪ 𝐹)) | 
| 13 | 12 | anbi2i 623 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑋)) ↔ (𝐽 ∈ Top ∧ (𝐹 ∈ ∪ ran Fil
∧ 𝑋 = ∪ 𝐹))) | 
| 14 | 13 | anbi1i 624 | . . 3
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)) ↔ ((𝐽 ∈ Top ∧ (𝐹 ∈ ∪ ran Fil
∧ 𝑋 = ∪ 𝐹))
∧ ∀𝑠 ∈
𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | 
| 15 |  | df-3an 1089 | . . 3
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)) ↔ ((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | 
| 16 |  | anass 468 | . . . 4
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) ↔ (𝐽 ∈ Top ∧ (𝐹 ∈ ∪ ran Fil
∧ 𝑋 = ∪ 𝐹))) | 
| 17 | 16 | anbi1i 624 | . . 3
⊢ ((((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)) ↔ ((𝐽 ∈ Top ∧ (𝐹 ∈ ∪ ran Fil
∧ 𝑋 = ∪ 𝐹))
∧ ∀𝑠 ∈
𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | 
| 18 | 14, 15, 17 | 3bitr4i 303 | . 2
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)) ↔ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran
Fil) ∧ 𝑋 = ∪ 𝐹)
∧ ∀𝑠 ∈
𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | 
| 19 |  | df-fcls 23949 | . . . 4
⊢  fClus =
(𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ if(∪ 𝑗 = ∪
𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅)) | 
| 20 | 19 | elmpocl 7674 | . . 3
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran
Fil)) | 
| 21 |  | fclsval.x | . . . . . . 7
⊢ 𝑋 = ∪
𝐽 | 
| 22 | 21 | fclsval 24016 | . . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘∪ 𝐹))
→ (𝐽 fClus 𝐹) = if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅)) | 
| 23 | 7, 22 | sylan2b 594 | . . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) → (𝐽 fClus 𝐹) = if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅)) | 
| 24 | 23 | eleq2d 2827 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ 𝐴 ∈ if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅))) | 
| 25 |  | n0i 4340 | . . . . . . 7
⊢ (𝐴 ∈ if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅) → ¬ if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅) = ∅) | 
| 26 |  | iffalse 4534 | . . . . . . 7
⊢ (¬
𝑋 = ∪ 𝐹
→ if(𝑋 = ∪ 𝐹,
∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅) = ∅) | 
| 27 | 25, 26 | nsyl2 141 | . . . . . 6
⊢ (𝐴 ∈ if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅) → 𝑋 = ∪ 𝐹) | 
| 28 | 27 | a1i 11 | . . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) → (𝐴 ∈ if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅) → 𝑋 = ∪ 𝐹)) | 
| 29 | 28 | pm4.71rd 562 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) → (𝐴 ∈ if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅) ↔ (𝑋 = ∪ 𝐹 ∧ 𝐴 ∈ if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅)))) | 
| 30 |  | iftrue 4531 | . . . . . . . 8
⊢ (𝑋 = ∪
𝐹 → if(𝑋 = ∪
𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅) = ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠)) | 
| 31 | 30 | adantl 481 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) → if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅) = ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠)) | 
| 32 | 31 | eleq2d 2827 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) → (𝐴 ∈ if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅) ↔ 𝐴 ∈ ∩
𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠))) | 
| 33 |  | elex 3501 | . . . . . . . 8
⊢ (𝐴 ∈ ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠) → 𝐴 ∈ V) | 
| 34 | 33 | a1i 11 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) → (𝐴 ∈ ∩
𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠) → 𝐴 ∈ V)) | 
| 35 |  | filn0 23870 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ 𝐹 ≠
∅) | 
| 36 | 7, 35 | sylbi 217 | . . . . . . . . . 10
⊢ (𝐹 ∈ ∪ ran Fil → 𝐹 ≠ ∅) | 
| 37 | 36 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) → 𝐹 ≠ ∅) | 
| 38 |  | r19.2z 4495 | . . . . . . . . . 10
⊢ ((𝐹 ≠ ∅ ∧
∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)) → ∃𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)) | 
| 39 | 38 | ex 412 | . . . . . . . . 9
⊢ (𝐹 ≠ ∅ →
(∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠) → ∃𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | 
| 40 | 37, 39 | syl 17 | . . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) → (∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠) → ∃𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | 
| 41 |  | elex 3501 | . . . . . . . . 9
⊢ (𝐴 ∈ ((cls‘𝐽)‘𝑠) → 𝐴 ∈ V) | 
| 42 | 41 | rexlimivw 3151 | . . . . . . . 8
⊢
(∃𝑠 ∈
𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠) → 𝐴 ∈ V) | 
| 43 | 40, 42 | syl6 35 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) → (∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠) → 𝐴 ∈ V)) | 
| 44 |  | eliin 4996 | . . . . . . . 8
⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠) ↔ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | 
| 45 | 44 | a1i 11 | . . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) → (𝐴 ∈ V → (𝐴 ∈ ∩
𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠) ↔ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)))) | 
| 46 | 34, 43, 45 | pm5.21ndd 379 | . . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) → (𝐴 ∈ ∩
𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠) ↔ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | 
| 47 | 32, 46 | bitrd 279 | . . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) ∧ 𝑋 = ∪ 𝐹) → (𝐴 ∈ if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅) ↔ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | 
| 48 | 47 | pm5.32da 579 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) → ((𝑋 = ∪ 𝐹 ∧ 𝐴 ∈ if(𝑋 = ∪ 𝐹, ∩ 𝑠 ∈ 𝐹 ((cls‘𝐽)‘𝑠), ∅)) ↔ (𝑋 = ∪ 𝐹 ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)))) | 
| 49 | 24, 29, 48 | 3bitrd 305 | . . 3
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝑋 = ∪ 𝐹 ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)))) | 
| 50 | 20, 49 | biadanii 822 | . 2
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran
Fil) ∧ (𝑋 = ∪ 𝐹
∧ ∀𝑠 ∈
𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)))) | 
| 51 | 1, 18, 50 | 3bitr4ri 304 | 1
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) |