| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfvex 6943 | . . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V) | 
| 2 |  | isust 24213 | . . . . . . 7
⊢ (𝑋 ∈ V → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))))) | 
| 3 | 1, 2 | syl 17 | . . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))))) | 
| 4 | 3 | ibi 267 | . . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))) | 
| 5 | 4 | adantl 481 | . . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))) | 
| 6 | 5 | simp1d 1142 | . . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ⊆ 𝒫 (𝑋 × 𝑋)) | 
| 7 | 5 | simp2d 1143 | . . . . 5
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑋 × 𝑋) ∈ 𝑈) | 
| 8 | 7 | ne0d 4341 | . . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ≠ ∅) | 
| 9 | 5 | simp3d 1144 | . . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))) | 
| 10 | 9 | r19.21bi 3250 | . . . . . . . . 9
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) → (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))) | 
| 11 | 10 | simp3d 1144 | . . . . . . . 8
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) → (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)) | 
| 12 | 11 | simp1d 1142 | . . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) → ( I ↾ 𝑋) ⊆ 𝑣) | 
| 13 |  | opelidres 6008 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ V → (〈𝑤, 𝑤〉 ∈ ( I ↾ 𝑋) ↔ 𝑤 ∈ 𝑋)) | 
| 14 | 13 | elv 3484 | . . . . . . . . . . . 12
⊢
(〈𝑤, 𝑤〉 ∈ ( I ↾ 𝑋) ↔ 𝑤 ∈ 𝑋) | 
| 15 | 14 | biimpri 228 | . . . . . . . . . . 11
⊢ (𝑤 ∈ 𝑋 → 〈𝑤, 𝑤〉 ∈ ( I ↾ 𝑋)) | 
| 16 | 15 | rgen 3062 | . . . . . . . . . 10
⊢
∀𝑤 ∈
𝑋 〈𝑤, 𝑤〉 ∈ ( I ↾ 𝑋) | 
| 17 |  | r19.2z 4494 | . . . . . . . . . 10
⊢ ((𝑋 ≠ ∅ ∧
∀𝑤 ∈ 𝑋 〈𝑤, 𝑤〉 ∈ ( I ↾ 𝑋)) → ∃𝑤 ∈ 𝑋 〈𝑤, 𝑤〉 ∈ ( I ↾ 𝑋)) | 
| 18 | 16, 17 | mpan2 691 | . . . . . . . . 9
⊢ (𝑋 ≠ ∅ →
∃𝑤 ∈ 𝑋 〈𝑤, 𝑤〉 ∈ ( I ↾ 𝑋)) | 
| 19 | 18 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) → ∃𝑤 ∈ 𝑋 〈𝑤, 𝑤〉 ∈ ( I ↾ 𝑋)) | 
| 20 |  | ne0i 4340 | . . . . . . . . 9
⊢
(〈𝑤, 𝑤〉 ∈ ( I ↾ 𝑋) → ( I ↾ 𝑋) ≠ ∅) | 
| 21 | 20 | rexlimivw 3150 | . . . . . . . 8
⊢
(∃𝑤 ∈
𝑋 〈𝑤, 𝑤〉 ∈ ( I ↾ 𝑋) → ( I ↾ 𝑋) ≠ ∅) | 
| 22 | 19, 21 | syl 17 | . . . . . . 7
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) → ( I ↾ 𝑋) ≠ ∅) | 
| 23 |  | ssn0 4403 | . . . . . . 7
⊢ ((( I
↾ 𝑋) ⊆ 𝑣 ∧ ( I ↾ 𝑋) ≠ ∅) → 𝑣 ≠ ∅) | 
| 24 | 12, 22, 23 | syl2anc 584 | . . . . . 6
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) → 𝑣 ≠ ∅) | 
| 25 | 24 | nelrdva 3710 | . . . . 5
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ¬ ∅ ∈
𝑈) | 
| 26 |  | df-nel 3046 | . . . . 5
⊢ (∅
∉ 𝑈 ↔ ¬
∅ ∈ 𝑈) | 
| 27 | 25, 26 | sylibr 234 | . . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∅ ∉ 𝑈) | 
| 28 | 10 | simp2d 1143 | . . . . . . . . 9
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) → ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈) | 
| 29 | 28 | r19.21bi 3250 | . . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) ∧ 𝑤 ∈ 𝑈) → (𝑣 ∩ 𝑤) ∈ 𝑈) | 
| 30 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑤 ∈ V | 
| 31 | 30 | inex2 5317 | . . . . . . . . . 10
⊢ (𝑣 ∩ 𝑤) ∈ V | 
| 32 | 31 | pwid 4621 | . . . . . . . . 9
⊢ (𝑣 ∩ 𝑤) ∈ 𝒫 (𝑣 ∩ 𝑤) | 
| 33 | 32 | a1i 11 | . . . . . . . 8
⊢ ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) ∧ 𝑤 ∈ 𝑈) → (𝑣 ∩ 𝑤) ∈ 𝒫 (𝑣 ∩ 𝑤)) | 
| 34 | 29, 33 | elind 4199 | . . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) ∧ 𝑤 ∈ 𝑈) → (𝑣 ∩ 𝑤) ∈ (𝑈 ∩ 𝒫 (𝑣 ∩ 𝑤))) | 
| 35 | 34 | ne0d 4341 | . . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) ∧ 𝑤 ∈ 𝑈) → (𝑈 ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅) | 
| 36 | 35 | ralrimiva 3145 | . . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) → ∀𝑤 ∈ 𝑈 (𝑈 ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅) | 
| 37 | 36 | ralrimiva 3145 | . . . 4
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∀𝑣 ∈ 𝑈 ∀𝑤 ∈ 𝑈 (𝑈 ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅) | 
| 38 | 8, 27, 37 | 3jca 1128 | . . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣 ∈ 𝑈 ∀𝑤 ∈ 𝑈 (𝑈 ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)) | 
| 39 | 1, 1 | xpexd 7772 | . . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ V) | 
| 40 |  | isfbas 23838 | . . . . 5
⊢ ((𝑋 × 𝑋) ∈ V → (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣 ∈ 𝑈 ∀𝑤 ∈ 𝑈 (𝑈 ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)))) | 
| 41 | 39, 40 | syl 17 | . . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣 ∈ 𝑈 ∀𝑤 ∈ 𝑈 (𝑈 ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)))) | 
| 42 | 41 | adantl 481 | . . 3
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑈 ≠ ∅ ∧ ∅ ∉ 𝑈 ∧ ∀𝑣 ∈ 𝑈 ∀𝑤 ∈ 𝑈 (𝑈 ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)))) | 
| 43 | 6, 38, 42 | mpbir2and 713 | . 2
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ∈ (fBas‘(𝑋 × 𝑋))) | 
| 44 |  | n0 4352 | . . . . 5
⊢ ((𝑈 ∩ 𝒫 𝑤) ≠ ∅ ↔
∃𝑣 𝑣 ∈ (𝑈 ∩ 𝒫 𝑤)) | 
| 45 |  | elin 3966 | . . . . . . 7
⊢ (𝑣 ∈ (𝑈 ∩ 𝒫 𝑤) ↔ (𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝒫 𝑤)) | 
| 46 |  | velpw 4604 | . . . . . . . 8
⊢ (𝑣 ∈ 𝒫 𝑤 ↔ 𝑣 ⊆ 𝑤) | 
| 47 | 46 | anbi2i 623 | . . . . . . 7
⊢ ((𝑣 ∈ 𝑈 ∧ 𝑣 ∈ 𝒫 𝑤) ↔ (𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤)) | 
| 48 | 45, 47 | bitri 275 | . . . . . 6
⊢ (𝑣 ∈ (𝑈 ∩ 𝒫 𝑤) ↔ (𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤)) | 
| 49 | 48 | exbii 1847 | . . . . 5
⊢
(∃𝑣 𝑣 ∈ (𝑈 ∩ 𝒫 𝑤) ↔ ∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤)) | 
| 50 | 44, 49 | bitri 275 | . . . 4
⊢ ((𝑈 ∩ 𝒫 𝑤) ≠ ∅ ↔
∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤)) | 
| 51 | 10 | simp1d 1142 | . . . . . . . 8
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) → ∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈)) | 
| 52 | 51 | r19.21bi 3250 | . . . . . . 7
⊢ ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑣 ∈ 𝑈) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → (𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈)) | 
| 53 | 52 | an32s 652 | . . . . . 6
⊢ ((((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) ∧ 𝑣 ∈ 𝑈) → (𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈)) | 
| 54 | 53 | expimpd 453 | . . . . 5
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → ((𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤) → 𝑤 ∈ 𝑈)) | 
| 55 | 54 | exlimdv 1932 | . . . 4
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → (∃𝑣(𝑣 ∈ 𝑈 ∧ 𝑣 ⊆ 𝑤) → 𝑤 ∈ 𝑈)) | 
| 56 | 50, 55 | biimtrid 242 | . . 3
⊢ (((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) ∧ 𝑤 ∈ 𝒫 (𝑋 × 𝑋)) → ((𝑈 ∩ 𝒫 𝑤) ≠ ∅ → 𝑤 ∈ 𝑈)) | 
| 57 | 56 | ralrimiva 3145 | . 2
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → ∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)((𝑈 ∩ 𝒫 𝑤) ≠ ∅ → 𝑤 ∈ 𝑈)) | 
| 58 |  | isfil 23856 | . 2
⊢ (𝑈 ∈ (Fil‘(𝑋 × 𝑋)) ↔ (𝑈 ∈ (fBas‘(𝑋 × 𝑋)) ∧ ∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)((𝑈 ∩ 𝒫 𝑤) ≠ ∅ → 𝑤 ∈ 𝑈))) | 
| 59 | 43, 57, 58 | sylanbrc 583 | 1
⊢ ((𝑋 ≠ ∅ ∧ 𝑈 ∈ (UnifOn‘𝑋)) → 𝑈 ∈ (Fil‘(𝑋 × 𝑋))) |