| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dffi2 9463 | . . . 4
⊢ (𝐹 ∈ (fBas‘𝑋) → (fi‘𝐹) = ∩
{𝑧 ∣ (𝐹 ⊆ 𝑧 ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (𝑢 ∩ 𝑣) ∈ 𝑧)}) | 
| 2 |  | sseq2 4010 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝑢 ∩ 𝑣) → (𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ (𝑢 ∩ 𝑣))) | 
| 3 | 2 | rexbidv 3179 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝑢 ∩ 𝑣) → (∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃𝑥 ∈ 𝐹 𝑥 ⊆ (𝑢 ∩ 𝑣))) | 
| 4 |  | inss1 4237 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∩ 𝑣) ⊆ 𝑢 | 
| 5 |  | simp1r 1199 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → 𝑢 ∈ 𝒫 ∪ 𝐹) | 
| 6 | 5 | elpwid 4609 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → 𝑢 ⊆ ∪ 𝐹) | 
| 7 | 4, 6 | sstrid 3995 | . . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → (𝑢 ∩ 𝑣) ⊆ ∪ 𝐹) | 
| 8 |  | vex 3484 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑢 ∈ V | 
| 9 | 8 | inex1 5317 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∩ 𝑣) ∈ V | 
| 10 | 9 | elpw 4604 | . . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∩ 𝑣) ∈ 𝒫 ∪ 𝐹
↔ (𝑢 ∩ 𝑣) ⊆ ∪ 𝐹) | 
| 11 | 7, 10 | sylibr 234 | . . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → (𝑢 ∩ 𝑣) ∈ 𝒫 ∪ 𝐹) | 
| 12 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
→ 𝐹 ∈
(fBas‘𝑋)) | 
| 13 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) → 𝑦 ∈ 𝐹) | 
| 14 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣) → 𝑧 ∈ 𝐹) | 
| 15 |  | fbasssin 23844 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹) → ∃𝑥 ∈ 𝐹 𝑥 ⊆ (𝑦 ∩ 𝑧)) | 
| 16 | 12, 13, 14, 15 | syl3an 1161 | . . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → ∃𝑥 ∈ 𝐹 𝑥 ⊆ (𝑦 ∩ 𝑧)) | 
| 17 |  | ss2in 4245 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 ⊆ 𝑢 ∧ 𝑧 ⊆ 𝑣) → (𝑦 ∩ 𝑧) ⊆ (𝑢 ∩ 𝑣)) | 
| 18 | 17 | ad2ant2l 746 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → (𝑦 ∩ 𝑧) ⊆ (𝑢 ∩ 𝑣)) | 
| 19 | 18 | 3adant1 1131 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → (𝑦 ∩ 𝑧) ⊆ (𝑢 ∩ 𝑣)) | 
| 20 |  | sstr 3992 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ⊆ (𝑦 ∩ 𝑧) ∧ (𝑦 ∩ 𝑧) ⊆ (𝑢 ∩ 𝑣)) → 𝑥 ⊆ (𝑢 ∩ 𝑣)) | 
| 21 | 20 | expcom 413 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∩ 𝑧) ⊆ (𝑢 ∩ 𝑣) → (𝑥 ⊆ (𝑦 ∩ 𝑧) → 𝑥 ⊆ (𝑢 ∩ 𝑣))) | 
| 22 | 19, 21 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → (𝑥 ⊆ (𝑦 ∩ 𝑧) → 𝑥 ⊆ (𝑢 ∩ 𝑣))) | 
| 23 | 22 | reximdv 3170 | . . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → (∃𝑥 ∈ 𝐹 𝑥 ⊆ (𝑦 ∩ 𝑧) → ∃𝑥 ∈ 𝐹 𝑥 ⊆ (𝑢 ∩ 𝑣))) | 
| 24 | 16, 23 | mpd 15 | . . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → ∃𝑥 ∈ 𝐹 𝑥 ⊆ (𝑢 ∩ 𝑣)) | 
| 25 | 3, 11, 24 | elrabd 3694 | . . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}) | 
| 26 | 25 | 3expa 1119 | . . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣)) → (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}) | 
| 27 | 26 | rexlimdvaa 3156 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢)) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 → (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 28 | 27 | ralrimivw 3150 | . . . . . . . . . . 11
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢)) → ∀𝑣 ∈ 𝒫 ∪ 𝐹(∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 → (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 29 |  | sseq2 4010 | . . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑣 → (𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ 𝑣)) | 
| 30 | 29 | rexbidv 3179 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑣 → (∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑣)) | 
| 31 |  | sseq1 4009 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝑥 ⊆ 𝑣 ↔ 𝑧 ⊆ 𝑣)) | 
| 32 | 31 | cbvrexvw 3238 | . . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑣 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣) | 
| 33 | 30, 32 | bitrdi 287 | . . . . . . . . . . . 12
⊢ (𝑡 = 𝑣 → (∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣)) | 
| 34 | 33 | ralrab 3699 | . . . . . . . . . . 11
⊢
(∀𝑣 ∈
{𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ↔ ∀𝑣 ∈ 𝒫 ∪ 𝐹(∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 → (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 35 | 28, 34 | sylibr 234 | . . . . . . . . . 10
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢)) → ∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}) | 
| 36 | 35 | rexlimdvaa 3156 | . . . . . . . . 9
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹)
→ (∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑢 → ∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 37 | 36 | ralrimiva 3146 | . . . . . . . 8
⊢ (𝐹 ∈ (fBas‘𝑋) → ∀𝑢 ∈ 𝒫 ∪ 𝐹(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 → ∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 38 |  | sseq2 4010 | . . . . . . . . . . 11
⊢ (𝑡 = 𝑢 → (𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ 𝑢)) | 
| 39 | 38 | rexbidv 3179 | . . . . . . . . . 10
⊢ (𝑡 = 𝑢 → (∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑢)) | 
| 40 |  | sseq1 4009 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝑢 ↔ 𝑦 ⊆ 𝑢)) | 
| 41 | 40 | cbvrexvw 3238 | . . . . . . . . . 10
⊢
(∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑢 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢) | 
| 42 | 39, 41 | bitrdi 287 | . . . . . . . . 9
⊢ (𝑡 = 𝑢 → (∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢)) | 
| 43 | 42 | ralrab 3699 | . . . . . . . 8
⊢
(∀𝑢 ∈
{𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ↔ ∀𝑢 ∈ 𝒫 ∪ 𝐹(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 → ∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 44 | 37, 43 | sylibr 234 | . . . . . . 7
⊢ (𝐹 ∈ (fBas‘𝑋) → ∀𝑢 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}) | 
| 45 |  | pwuni 4945 | . . . . . . . 8
⊢ 𝐹 ⊆ 𝒫 ∪ 𝐹 | 
| 46 |  | ssid 4006 | . . . . . . . . . 10
⊢ 𝑡 ⊆ 𝑡 | 
| 47 |  | sseq1 4009 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑡 → (𝑥 ⊆ 𝑡 ↔ 𝑡 ⊆ 𝑡)) | 
| 48 | 47 | rspcev 3622 | . . . . . . . . . 10
⊢ ((𝑡 ∈ 𝐹 ∧ 𝑡 ⊆ 𝑡) → ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡) | 
| 49 | 46, 48 | mpan2 691 | . . . . . . . . 9
⊢ (𝑡 ∈ 𝐹 → ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡) | 
| 50 | 49 | rgen 3063 | . . . . . . . 8
⊢
∀𝑡 ∈
𝐹 ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 | 
| 51 |  | ssrab 4073 | . . . . . . . 8
⊢ (𝐹 ⊆ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ↔ (𝐹 ⊆ 𝒫 ∪ 𝐹
∧ ∀𝑡 ∈
𝐹 ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡)) | 
| 52 | 45, 50, 51 | mpbir2an 711 | . . . . . . 7
⊢ 𝐹 ⊆ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} | 
| 53 | 44, 52 | jctil 519 | . . . . . 6
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝐹 ⊆ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ∧ ∀𝑢 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 54 |  | uniexg 7760 | . . . . . . 7
⊢ (𝐹 ∈ (fBas‘𝑋) → ∪ 𝐹
∈ V) | 
| 55 |  | pwexg 5378 | . . . . . . 7
⊢ (∪ 𝐹
∈ V → 𝒫 ∪ 𝐹 ∈ V) | 
| 56 |  | rabexg 5337 | . . . . . . 7
⊢
(𝒫 ∪ 𝐹 ∈ V → {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ∈ V) | 
| 57 |  | sseq2 4010 | . . . . . . . . 9
⊢ (𝑧 = {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} → (𝐹 ⊆ 𝑧 ↔ 𝐹 ⊆ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 58 |  | eleq2 2830 | . . . . . . . . . . 11
⊢ (𝑧 = {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} → ((𝑢 ∩ 𝑣) ∈ 𝑧 ↔ (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 59 | 58 | raleqbi1dv 3338 | . . . . . . . . . 10
⊢ (𝑧 = {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} → (∀𝑣 ∈ 𝑧 (𝑢 ∩ 𝑣) ∈ 𝑧 ↔ ∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 60 | 59 | raleqbi1dv 3338 | . . . . . . . . 9
⊢ (𝑧 = {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} → (∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (𝑢 ∩ 𝑣) ∈ 𝑧 ↔ ∀𝑢 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡})) | 
| 61 | 57, 60 | anbi12d 632 | . . . . . . . 8
⊢ (𝑧 = {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} → ((𝐹 ⊆ 𝑧 ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (𝑢 ∩ 𝑣) ∈ 𝑧) ↔ (𝐹 ⊆ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ∧ ∀𝑢 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}))) | 
| 62 | 61 | elabg 3676 | . . . . . . 7
⊢ ({𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ∈ V → ({𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ∈ {𝑧 ∣ (𝐹 ⊆ 𝑧 ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (𝑢 ∩ 𝑣) ∈ 𝑧)} ↔ (𝐹 ⊆ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ∧ ∀𝑢 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}))) | 
| 63 | 54, 55, 56, 62 | 4syl 19 | . . . . . 6
⊢ (𝐹 ∈ (fBas‘𝑋) → ({𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ∈ {𝑧 ∣ (𝐹 ⊆ 𝑧 ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (𝑢 ∩ 𝑣) ∈ 𝑧)} ↔ (𝐹 ⊆ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ∧ ∀𝑢 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}∀𝑣 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} (𝑢 ∩ 𝑣) ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}))) | 
| 64 | 53, 63 | mpbird 257 | . . . . 5
⊢ (𝐹 ∈ (fBas‘𝑋) → {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ∈ {𝑧 ∣ (𝐹 ⊆ 𝑧 ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (𝑢 ∩ 𝑣) ∈ 𝑧)}) | 
| 65 |  | intss1 4963 | . . . . 5
⊢ ({𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ∈ {𝑧 ∣ (𝐹 ⊆ 𝑧 ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (𝑢 ∩ 𝑣) ∈ 𝑧)} → ∩ {𝑧 ∣ (𝐹 ⊆ 𝑧 ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (𝑢 ∩ 𝑣) ∈ 𝑧)} ⊆ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}) | 
| 66 | 64, 65 | syl 17 | . . . 4
⊢ (𝐹 ∈ (fBas‘𝑋) → ∩ {𝑧
∣ (𝐹 ⊆ 𝑧 ∧ ∀𝑢 ∈ 𝑧 ∀𝑣 ∈ 𝑧 (𝑢 ∩ 𝑣) ∈ 𝑧)} ⊆ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}) | 
| 67 | 1, 66 | eqsstrd 4018 | . . 3
⊢ (𝐹 ∈ (fBas‘𝑋) → (fi‘𝐹) ⊆ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}) | 
| 68 | 67 | sselda 3983 | . 2
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐴 ∈ (fi‘𝐹)) → 𝐴 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡}) | 
| 69 |  | sseq2 4010 | . . . . 5
⊢ (𝑡 = 𝐴 → (𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ 𝐴)) | 
| 70 | 69 | rexbidv 3179 | . . . 4
⊢ (𝑡 = 𝐴 → (∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴)) | 
| 71 | 70 | elrab 3692 | . . 3
⊢ (𝐴 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} ↔ (𝐴 ∈ 𝒫 ∪ 𝐹
∧ ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴)) | 
| 72 | 71 | simprbi 496 | . 2
⊢ (𝐴 ∈ {𝑡 ∈ 𝒫 ∪ 𝐹
∣ ∃𝑥 ∈
𝐹 𝑥 ⊆ 𝑡} → ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴) | 
| 73 | 68, 72 | syl 17 | 1
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐴 ∈ (fi‘𝐹)) → ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴) |