| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfg 23880 | . 2
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ (𝑋filGen𝐹) ↔ (𝑧 ⊆ 𝑋 ∧ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧))) | 
| 2 |  | elfvex 6943 | . 2
⊢ (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ V) | 
| 3 |  | fbasne0 23839 | . . . . . 6
⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ≠ ∅) | 
| 4 |  | n0 4352 | . . . . . 6
⊢ (𝐹 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐹) | 
| 5 | 3, 4 | sylib 218 | . . . . 5
⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 𝑦 ∈ 𝐹) | 
| 6 |  | fbelss 23842 | . . . . . . . 8
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋) | 
| 7 | 6 | ex 412 | . . . . . . 7
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑦 ∈ 𝐹 → 𝑦 ⊆ 𝑋)) | 
| 8 | 7 | ancld 550 | . . . . . 6
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑦 ∈ 𝐹 → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋))) | 
| 9 | 8 | eximdv 1916 | . . . . 5
⊢ (𝐹 ∈ (fBas‘𝑋) → (∃𝑦 𝑦 ∈ 𝐹 → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋))) | 
| 10 | 5, 9 | mpd 15 | . . . 4
⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋)) | 
| 11 |  | df-rex 3070 | . . . 4
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑋 ↔ ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋)) | 
| 12 | 10, 11 | sylibr 234 | . . 3
⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋) | 
| 13 |  | elfvdm 6942 | . . . 4
⊢ (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ dom fBas) | 
| 14 |  | sseq2 4009 | . . . . . 6
⊢ (𝑧 = 𝑋 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑋)) | 
| 15 | 14 | rexbidv 3178 | . . . . 5
⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋)) | 
| 16 | 15 | sbcieg 3827 | . . . 4
⊢ (𝑋 ∈ dom fBas →
([𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋)) | 
| 17 | 13, 16 | syl 17 | . . 3
⊢ (𝐹 ∈ (fBas‘𝑋) → ([𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋)) | 
| 18 | 12, 17 | mpbird 257 | . 2
⊢ (𝐹 ∈ (fBas‘𝑋) → [𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) | 
| 19 |  | 0nelfb 23840 | . . 3
⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ ∅ ∈
𝐹) | 
| 20 |  | 0ex 5306 | . . . . 5
⊢ ∅
∈ V | 
| 21 |  | sseq2 4009 | . . . . . 6
⊢ (𝑧 = ∅ → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ ∅)) | 
| 22 | 21 | rexbidv 3178 | . . . . 5
⊢ (𝑧 = ∅ → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅)) | 
| 23 | 20, 22 | sbcie 3829 | . . . 4
⊢
([∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅) | 
| 24 |  | ss0 4401 | . . . . . . 7
⊢ (𝑦 ⊆ ∅ → 𝑦 = ∅) | 
| 25 | 24 | eleq1d 2825 | . . . . . 6
⊢ (𝑦 ⊆ ∅ → (𝑦 ∈ 𝐹 ↔ ∅ ∈ 𝐹)) | 
| 26 | 25 | biimpac 478 | . . . . 5
⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ ∅) → ∅ ∈ 𝐹) | 
| 27 | 26 | rexlimiva 3146 | . . . 4
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ ∅ → ∅ ∈ 𝐹) | 
| 28 | 23, 27 | sylbi 217 | . . 3
⊢
([∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → ∅ ∈ 𝐹) | 
| 29 | 19, 28 | nsyl 140 | . 2
⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ [∅ /
𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) | 
| 30 |  | sstr 3991 | . . . . . 6
⊢ ((𝑦 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑢) → 𝑦 ⊆ 𝑢) | 
| 31 | 30 | expcom 413 | . . . . 5
⊢ (𝑣 ⊆ 𝑢 → (𝑦 ⊆ 𝑣 → 𝑦 ⊆ 𝑢)) | 
| 32 | 31 | reximdv 3169 | . . . 4
⊢ (𝑣 ⊆ 𝑢 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢)) | 
| 33 | 32 | 3ad2ant3 1135 | . . 3
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢)) | 
| 34 |  | vex 3483 | . . . 4
⊢ 𝑣 ∈ V | 
| 35 |  | sseq2 4009 | . . . . 5
⊢ (𝑧 = 𝑣 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑣)) | 
| 36 | 35 | rexbidv 3178 | . . . 4
⊢ (𝑧 = 𝑣 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣)) | 
| 37 | 34, 36 | sbcie 3829 | . . 3
⊢
([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣) | 
| 38 |  | vex 3483 | . . . 4
⊢ 𝑢 ∈ V | 
| 39 |  | sseq2 4009 | . . . . 5
⊢ (𝑧 = 𝑢 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑢)) | 
| 40 | 39 | rexbidv 3178 | . . . 4
⊢ (𝑧 = 𝑢 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢)) | 
| 41 | 38, 40 | sbcie 3829 | . . 3
⊢
([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢) | 
| 42 | 33, 37, 41 | 3imtr4g 296 | . 2
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢) → ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → [𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)) | 
| 43 |  | fbasssin 23845 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤)) | 
| 44 | 43 | 3expib 1122 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (fBas‘𝑋) → ((𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤))) | 
| 45 |  | sstr2 3989 | . . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → 𝑦 ⊆ (𝑢 ∩ 𝑣))) | 
| 46 | 45 | com12 32 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (𝑦 ⊆ (𝑧 ∩ 𝑤) → 𝑦 ⊆ (𝑢 ∩ 𝑣))) | 
| 47 | 46 | reximdv 3169 | . . . . . . . . . . . 12
⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) | 
| 48 |  | ss2in 4244 | . . . . . . . . . . . 12
⊢ ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)) | 
| 49 | 47, 48 | syl11 33 | . . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) | 
| 50 | 44, 49 | syl6 35 | . . . . . . . . . 10
⊢ (𝐹 ∈ (fBas‘𝑋) → ((𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))) | 
| 51 | 50 | exp5c 444 | . . . . . . . . 9
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ 𝐹 → (𝑤 ∈ 𝐹 → (𝑧 ⊆ 𝑢 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))))) | 
| 52 | 51 | imp31 417 | . . . . . . . 8
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑤 ∈ 𝐹) → (𝑧 ⊆ 𝑢 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))) | 
| 53 | 52 | impancom 451 | . . . . . . 7
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑧 ⊆ 𝑢) → (𝑤 ∈ 𝐹 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))) | 
| 54 | 53 | rexlimdv 3152 | . . . . . 6
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑧 ⊆ 𝑢) → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) | 
| 55 | 54 | rexlimdva2 3156 | . . . . 5
⊢ (𝐹 ∈ (fBas‘𝑋) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))) | 
| 56 | 55 | impd 410 | . . . 4
⊢ (𝐹 ∈ (fBas‘𝑋) → ((∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) | 
| 57 | 56 | 3ad2ant1 1133 | . . 3
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋) → ((∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) | 
| 58 |  | sseq1 4008 | . . . . . 6
⊢ (𝑦 = 𝑧 → (𝑦 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑢)) | 
| 59 | 58 | cbvrexvw 3237 | . . . . 5
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑢 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢) | 
| 60 | 41, 59 | bitri 275 | . . . 4
⊢
([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢) | 
| 61 |  | sseq1 4008 | . . . . . 6
⊢ (𝑦 = 𝑤 → (𝑦 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑣)) | 
| 62 | 61 | cbvrexvw 3237 | . . . . 5
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑣 ↔ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) | 
| 63 | 37, 62 | bitri 275 | . . . 4
⊢
([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) | 
| 64 | 60, 63 | anbi12i 628 | . . 3
⊢
(([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) ↔ (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)) | 
| 65 | 38 | inex1 5316 | . . . 4
⊢ (𝑢 ∩ 𝑣) ∈ V | 
| 66 |  | sseq2 4009 | . . . . 5
⊢ (𝑧 = (𝑢 ∩ 𝑣) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑢 ∩ 𝑣))) | 
| 67 | 66 | rexbidv 3178 | . . . 4
⊢ (𝑧 = (𝑢 ∩ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) | 
| 68 | 65, 67 | sbcie 3829 | . . 3
⊢
([(𝑢 ∩
𝑣) / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)) | 
| 69 | 57, 64, 68 | 3imtr4g 296 | . 2
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋) → (([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) → [(𝑢 ∩ 𝑣) / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)) | 
| 70 | 1, 2, 18, 29, 42, 69 | isfild 23867 | 1
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |