Step | Hyp | Ref
| Expression |
1 | | elfg 21485 |
. 2
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ (𝑋filGen𝐹) ↔ (𝑧 ⊆ 𝑋 ∧ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧))) |
2 | | elfvex 6131 |
. 2
⊢ (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ V) |
3 | | fbasne0 21444 |
. . . . . 6
⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ≠ ∅) |
4 | | n0 3890 |
. . . . . 6
⊢ (𝐹 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐹) |
5 | 3, 4 | sylib 207 |
. . . . 5
⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 𝑦 ∈ 𝐹) |
6 | | fbelss 21447 |
. . . . . . . 8
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑦 ∈ 𝐹) → 𝑦 ⊆ 𝑋) |
7 | 6 | ex 449 |
. . . . . . 7
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑦 ∈ 𝐹 → 𝑦 ⊆ 𝑋)) |
8 | 7 | ancld 574 |
. . . . . 6
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑦 ∈ 𝐹 → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋))) |
9 | 8 | eximdv 1833 |
. . . . 5
⊢ (𝐹 ∈ (fBas‘𝑋) → (∃𝑦 𝑦 ∈ 𝐹 → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋))) |
10 | 5, 9 | mpd 15 |
. . . 4
⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋)) |
11 | | df-rex 2902 |
. . . 4
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑋 ↔ ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋)) |
12 | 10, 11 | sylibr 223 |
. . 3
⊢ (𝐹 ∈ (fBas‘𝑋) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋) |
13 | | elfvdm 6130 |
. . . 4
⊢ (𝐹 ∈ (fBas‘𝑋) → 𝑋 ∈ dom fBas) |
14 | | sseq2 3590 |
. . . . . 6
⊢ (𝑧 = 𝑋 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑋)) |
15 | 14 | rexbidv 3034 |
. . . . 5
⊢ (𝑧 = 𝑋 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋)) |
16 | 15 | sbcieg 3435 |
. . . 4
⊢ (𝑋 ∈ dom fBas →
([𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋)) |
17 | 13, 16 | syl 17 |
. . 3
⊢ (𝐹 ∈ (fBas‘𝑋) → ([𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑋)) |
18 | 12, 17 | mpbird 246 |
. 2
⊢ (𝐹 ∈ (fBas‘𝑋) → [𝑋 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) |
19 | | 0nelfb 21445 |
. . 3
⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ ∅ ∈
𝐹) |
20 | | 0ex 4718 |
. . . . 5
⊢ ∅
∈ V |
21 | | sseq2 3590 |
. . . . . 6
⊢ (𝑧 = ∅ → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ ∅)) |
22 | 21 | rexbidv 3034 |
. . . . 5
⊢ (𝑧 = ∅ → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅)) |
23 | 20, 22 | sbcie 3437 |
. . . 4
⊢
([∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ ∅) |
24 | | ss0 3926 |
. . . . . . 7
⊢ (𝑦 ⊆ ∅ → 𝑦 = ∅) |
25 | 24 | eleq1d 2672 |
. . . . . 6
⊢ (𝑦 ⊆ ∅ → (𝑦 ∈ 𝐹 ↔ ∅ ∈ 𝐹)) |
26 | 25 | biimpac 502 |
. . . . 5
⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ ∅) → ∅ ∈ 𝐹) |
27 | 26 | rexlimiva 3010 |
. . . 4
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ ∅ → ∅ ∈ 𝐹) |
28 | 23, 27 | sylbi 206 |
. . 3
⊢
([∅ / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → ∅ ∈ 𝐹) |
29 | 19, 28 | nsyl 134 |
. 2
⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ [∅ /
𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) |
30 | | sstr 3576 |
. . . . . 6
⊢ ((𝑦 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑢) → 𝑦 ⊆ 𝑢) |
31 | 30 | expcom 450 |
. . . . 5
⊢ (𝑣 ⊆ 𝑢 → (𝑦 ⊆ 𝑣 → 𝑦 ⊆ 𝑢)) |
32 | 31 | reximdv 2999 |
. . . 4
⊢ (𝑣 ⊆ 𝑢 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢)) |
33 | 32 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢)) |
34 | | vex 3176 |
. . . 4
⊢ 𝑣 ∈ V |
35 | | sseq2 3590 |
. . . . 5
⊢ (𝑧 = 𝑣 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑣)) |
36 | 35 | rexbidv 3034 |
. . . 4
⊢ (𝑧 = 𝑣 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣)) |
37 | 34, 36 | sbcie 3437 |
. . 3
⊢
([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑣) |
38 | | vex 3176 |
. . . 4
⊢ 𝑢 ∈ V |
39 | | sseq2 3590 |
. . . . 5
⊢ (𝑧 = 𝑢 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑢)) |
40 | 39 | rexbidv 3034 |
. . . 4
⊢ (𝑧 = 𝑢 → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢)) |
41 | 38, 40 | sbcie 3437 |
. . 3
⊢
([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢) |
42 | 33, 37, 41 | 3imtr4g 284 |
. 2
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑢) → ([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 → [𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)) |
43 | | fbasssin 21450 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤)) |
44 | 43 | 3expib 1260 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (fBas‘𝑋) → ((𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤))) |
45 | | ss2in 3802 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → (𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣)) |
46 | | sstr2 3575 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → 𝑦 ⊆ (𝑢 ∩ 𝑣))) |
47 | 46 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (𝑦 ⊆ (𝑧 ∩ 𝑤) → 𝑦 ⊆ (𝑢 ∩ 𝑣))) |
48 | 47 | reximdv 2999 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∩ 𝑤) ⊆ (𝑢 ∩ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) |
49 | 45, 48 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) |
50 | 49 | com12 32 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ (𝑧 ∩ 𝑤) → ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) |
51 | 44, 50 | syl6 34 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (fBas‘𝑋) → ((𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹) → ((𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))) |
52 | 51 | exp5c 642 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑧 ∈ 𝐹 → (𝑤 ∈ 𝐹 → (𝑧 ⊆ 𝑢 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))))) |
53 | 52 | imp31 447 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑤 ∈ 𝐹) → (𝑧 ⊆ 𝑢 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))) |
54 | 53 | impancom 455 |
. . . . . . . 8
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑧 ⊆ 𝑢) → (𝑤 ∈ 𝐹 → (𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))) |
55 | 54 | rexlimdv 3012 |
. . . . . . 7
⊢ (((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) ∧ 𝑧 ⊆ 𝑢) → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) |
56 | 55 | ex 449 |
. . . . . 6
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑧 ∈ 𝐹) → (𝑧 ⊆ 𝑢 → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))) |
57 | 56 | rexlimdva 3013 |
. . . . 5
⊢ (𝐹 ∈ (fBas‘𝑋) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 → (∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣 → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)))) |
58 | 57 | impd 446 |
. . . 4
⊢ (𝐹 ∈ (fBas‘𝑋) → ((∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) |
59 | 58 | 3ad2ant1 1075 |
. . 3
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋) → ((∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) → ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) |
60 | | sseq1 3589 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝑦 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑢)) |
61 | 60 | cbvrexv 3148 |
. . . . 5
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑢 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢) |
62 | 41, 61 | bitri 263 |
. . . 4
⊢
([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢) |
63 | | sseq1 3589 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (𝑦 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑣)) |
64 | 63 | cbvrexv 3148 |
. . . . 5
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑣 ↔ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) |
65 | 37, 64 | bitri 263 |
. . . 4
⊢
([𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣) |
66 | 62, 65 | anbi12i 729 |
. . 3
⊢
(([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) ↔ (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑢 ∧ ∃𝑤 ∈ 𝐹 𝑤 ⊆ 𝑣)) |
67 | 38 | inex1 4727 |
. . . 4
⊢ (𝑢 ∩ 𝑣) ∈ V |
68 | | sseq2 3590 |
. . . . 5
⊢ (𝑧 = (𝑢 ∩ 𝑣) → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ (𝑢 ∩ 𝑣))) |
69 | 68 | rexbidv 3034 |
. . . 4
⊢ (𝑧 = (𝑢 ∩ 𝑣) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣))) |
70 | 67, 69 | sbcie 3437 |
. . 3
⊢
([(𝑢 ∩
𝑣) / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ↔ ∃𝑦 ∈ 𝐹 𝑦 ⊆ (𝑢 ∩ 𝑣)) |
71 | 59, 66, 70 | 3imtr4g 284 |
. 2
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝑢 ⊆ 𝑋 ∧ 𝑣 ⊆ 𝑋) → (([𝑢 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧 ∧ [𝑣 / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧) → [(𝑢 ∩ 𝑣) / 𝑧]∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑧)) |
72 | 1, 2, 18, 29, 42, 71 | isfild 21472 |
1
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) |