Step |
Hyp |
Ref |
Expression |
1 |
|
dffi2 |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ 𝐹 ) = ∩ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } ) |
2 |
|
sseq2 |
⊢ ( 𝑡 = ( 𝑢 ∩ 𝑣 ) → ( 𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) |
3 |
2
|
rexbidv |
⊢ ( 𝑡 = ( 𝑢 ∩ 𝑣 ) → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) |
4 |
|
inss1 |
⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢 |
5 |
|
simp1r |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → 𝑢 ∈ 𝒫 ∪ 𝐹 ) |
6 |
5
|
elpwid |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → 𝑢 ⊆ ∪ 𝐹 ) |
7 |
4 6
|
sstrid |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ⊆ ∪ 𝐹 ) |
8 |
|
vex |
⊢ 𝑢 ∈ V |
9 |
8
|
inex1 |
⊢ ( 𝑢 ∩ 𝑣 ) ∈ V |
10 |
9
|
elpw |
⊢ ( ( 𝑢 ∩ 𝑣 ) ∈ 𝒫 ∪ 𝐹 ↔ ( 𝑢 ∩ 𝑣 ) ⊆ ∪ 𝐹 ) |
11 |
7 10
|
sylibr |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ∈ 𝒫 ∪ 𝐹 ) |
12 |
|
simpl |
⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) ) |
13 |
|
simpl |
⊢ ( ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) → 𝑦 ∈ 𝐹 ) |
14 |
|
simpl |
⊢ ( ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) → 𝑧 ∈ 𝐹 ) |
15 |
|
fbasssin |
⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) |
16 |
12 13 14 15
|
syl3an |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) |
17 |
|
ss2in |
⊢ ( ( 𝑦 ⊆ 𝑢 ∧ 𝑧 ⊆ 𝑣 ) → ( 𝑦 ∩ 𝑧 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) |
18 |
17
|
ad2ant2l |
⊢ ( ( ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑦 ∩ 𝑧 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) |
19 |
18
|
3adant1 |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑦 ∩ 𝑧 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) |
20 |
|
sstr |
⊢ ( ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ∧ ( 𝑦 ∩ 𝑧 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) → 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) |
21 |
20
|
expcom |
⊢ ( ( 𝑦 ∩ 𝑧 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) → 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) |
22 |
19 21
|
syl |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) → 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) |
23 |
22
|
reximdv |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) |
24 |
16 23
|
mpd |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑢 ∩ 𝑣 ) ) |
25 |
3 11 24
|
elrabd |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) |
26 |
25
|
3expa |
⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑣 ) ) → ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) |
27 |
26
|
rexlimdvaa |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ) → ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 → ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
28 |
27
|
ralrimivw |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ) → ∀ 𝑣 ∈ 𝒫 ∪ 𝐹 ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 → ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
29 |
|
sseq2 |
⊢ ( 𝑡 = 𝑣 → ( 𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ 𝑣 ) ) |
30 |
29
|
rexbidv |
⊢ ( 𝑡 = 𝑣 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑣 ) ) |
31 |
|
sseq1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 ⊆ 𝑣 ↔ 𝑧 ⊆ 𝑣 ) ) |
32 |
31
|
cbvrexvw |
⊢ ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑣 ↔ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 ) |
33 |
30 32
|
bitrdi |
⊢ ( 𝑡 = 𝑣 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 ) ) |
34 |
33
|
ralrab |
⊢ ( ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ↔ ∀ 𝑣 ∈ 𝒫 ∪ 𝐹 ( ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ 𝑣 → ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
35 |
28 34
|
sylibr |
⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑢 ) ) → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) |
36 |
35
|
rexlimdvaa |
⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑢 ∈ 𝒫 ∪ 𝐹 ) → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
37 |
36
|
ralrimiva |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∀ 𝑢 ∈ 𝒫 ∪ 𝐹 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
38 |
|
sseq2 |
⊢ ( 𝑡 = 𝑢 → ( 𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ 𝑢 ) ) |
39 |
38
|
rexbidv |
⊢ ( 𝑡 = 𝑢 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑢 ) ) |
40 |
|
sseq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝑢 ↔ 𝑦 ⊆ 𝑢 ) ) |
41 |
40
|
cbvrexvw |
⊢ ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑢 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 ) |
42 |
39 41
|
bitrdi |
⊢ ( 𝑡 = 𝑢 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 ) ) |
43 |
42
|
ralrab |
⊢ ( ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ↔ ∀ 𝑢 ∈ 𝒫 ∪ 𝐹 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑢 → ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
44 |
37 43
|
sylibr |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) |
45 |
|
pwuni |
⊢ 𝐹 ⊆ 𝒫 ∪ 𝐹 |
46 |
|
ssid |
⊢ 𝑡 ⊆ 𝑡 |
47 |
|
sseq1 |
⊢ ( 𝑥 = 𝑡 → ( 𝑥 ⊆ 𝑡 ↔ 𝑡 ⊆ 𝑡 ) ) |
48 |
47
|
rspcev |
⊢ ( ( 𝑡 ∈ 𝐹 ∧ 𝑡 ⊆ 𝑡 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) |
49 |
46 48
|
mpan2 |
⊢ ( 𝑡 ∈ 𝐹 → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) |
50 |
49
|
rgen |
⊢ ∀ 𝑡 ∈ 𝐹 ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 |
51 |
|
ssrab |
⊢ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ↔ ( 𝐹 ⊆ 𝒫 ∪ 𝐹 ∧ ∀ 𝑡 ∈ 𝐹 ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) ) |
52 |
45 50 51
|
mpbir2an |
⊢ 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } |
53 |
44 52
|
jctil |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
54 |
|
uniexg |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∪ 𝐹 ∈ V ) |
55 |
|
pwexg |
⊢ ( ∪ 𝐹 ∈ V → 𝒫 ∪ 𝐹 ∈ V ) |
56 |
|
rabexg |
⊢ ( 𝒫 ∪ 𝐹 ∈ V → { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ V ) |
57 |
|
sseq2 |
⊢ ( 𝑧 = { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ( 𝐹 ⊆ 𝑧 ↔ 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
58 |
|
eleq2 |
⊢ ( 𝑧 = { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ( ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ↔ ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
59 |
58
|
raleqbi1dv |
⊢ ( 𝑧 = { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ( ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ↔ ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
60 |
59
|
raleqbi1dv |
⊢ ( 𝑧 = { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ( ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ↔ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) |
61 |
57 60
|
anbi12d |
⊢ ( 𝑧 = { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ( ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) ↔ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) ) |
62 |
61
|
elabg |
⊢ ( { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ V → ( { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } ↔ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) ) |
63 |
54 55 56 62
|
4syl |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } ↔ ( 𝐹 ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∧ ∀ 𝑢 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∀ 𝑣 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ( 𝑢 ∩ 𝑣 ) ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) ) ) |
64 |
53 63
|
mpbird |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } ) |
65 |
|
intss1 |
⊢ ( { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ∈ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } → ∩ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) |
66 |
64 65
|
syl |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∩ { 𝑧 ∣ ( 𝐹 ⊆ 𝑧 ∧ ∀ 𝑢 ∈ 𝑧 ∀ 𝑣 ∈ 𝑧 ( 𝑢 ∩ 𝑣 ) ∈ 𝑧 ) } ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) |
67 |
1 66
|
eqsstrd |
⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( fi ‘ 𝐹 ) ⊆ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) |
68 |
67
|
sselda |
⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ ( fi ‘ 𝐹 ) ) → 𝐴 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ) |
69 |
|
sseq2 |
⊢ ( 𝑡 = 𝐴 → ( 𝑥 ⊆ 𝑡 ↔ 𝑥 ⊆ 𝐴 ) ) |
70 |
69
|
rexbidv |
⊢ ( 𝑡 = 𝐴 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) ) |
71 |
70
|
elrab |
⊢ ( 𝐴 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } ↔ ( 𝐴 ∈ 𝒫 ∪ 𝐹 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) ) |
72 |
71
|
simprbi |
⊢ ( 𝐴 ∈ { 𝑡 ∈ 𝒫 ∪ 𝐹 ∣ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 } → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) |
73 |
68 72
|
syl |
⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ ( fi ‘ 𝐹 ) ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) |