Metamath Proof Explorer

Theorem trfbas2

Description: Conditions for the trace of a filter base F to be a filter base. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion trfbas2 ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑌 ) → 𝑌 ∈ dom fBas )
2 ssexg ⊢ ( ( 𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ dom fBas ) → 𝐴 ∈ V )
3 2 ancoms ⊢ ( ( 𝑌 ∈ dom fBas ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ V )
4 1 3 sylan ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ V )
5 restsspw ⊢ ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝐴
6 5 a1i ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝐴 )
7 fbasne0 ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑌 ) → 𝐹 ≠ ∅ )
8 7 adantr ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐹 ≠ ∅ )
9 n0 ⊢ ( 𝐹 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐹 )
10 8 9 sylib ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ∃ 𝑥 𝑥 ∈ 𝐹 )
11 elrestr ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ∈ V ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) )
12 11 3expia ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ 𝐹 → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) ) )
13 4 12 syldan ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑥 ∈ 𝐹 → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) ) )
14 ne0i ⊢ ( ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) → ( 𝐹 ↾t 𝐴 ) ≠ ∅ )
15 13 14 syl6 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑥 ∈ 𝐹 → ( 𝐹 ↾t 𝐴 ) ≠ ∅ ) )
16 15 exlimdv ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∃ 𝑥 𝑥 ∈ 𝐹 → ( 𝐹 ↾t 𝐴 ) ≠ ∅ ) )
17 10 16 mpd ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝐹 ↾t 𝐴 ) ≠ ∅ )
18 fbasssin ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) )
19 18 3expb ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) )
20 19 adantlr ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) )
21 simplll ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) ) ) → 𝐹 ∈ ( fBas ‘ 𝑌 ) )
22 4 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) ) ) → 𝐴 ∈ V )
23 simprl ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) ) ) → 𝑥 ∈ 𝐹 )
24 21 22 23 11 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) ) ) → ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) )
25 ssrin ⊢ ( 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) → ( 𝑥 ∩ 𝐴 ) ⊆ ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) )
26 25 ad2antll ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) ) ) → ( 𝑥 ∩ 𝐴 ) ⊆ ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) )
27 vex ⊢ 𝑥 ∈ V
28 27 inex1 ⊢ ( 𝑥 ∩ 𝐴 ) ∈ V
29 28 elpw ⊢ ( ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ↔ ( 𝑥 ∩ 𝐴 ) ⊆ ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) )
30 26 29 sylibr ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) ) ) → ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) )
31 inelcm ⊢ ( ( ( 𝑥 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) ∧ ( 𝑥 ∩ 𝐴 ) ∈ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ) → ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ) ≠ ∅ )
32 24 30 31 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ ( 𝑧 ∩ 𝑤 ) ) ) → ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ) ≠ ∅ )
33 20 32 rexlimddv ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑤 ∈ 𝐹 ) ) → ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ) ≠ ∅ )
34 33 ralrimivva ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ∀ 𝑧 ∈ 𝐹 ∀ 𝑤 ∈ 𝐹 ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ) ≠ ∅ )
35 vex ⊢ 𝑧 ∈ V
36 35 inex1 ⊢ ( 𝑧 ∩ 𝐴 ) ∈ V
37 36 a1i ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑧 ∈ 𝐹 ) → ( 𝑧 ∩ 𝐴 ) ∈ V )
38 elrest ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( 𝐹 ↾t 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐹 𝑥 = ( 𝑧 ∩ 𝐴 ) ) )
39 4 38 syldan ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑥 ∈ ( 𝐹 ↾t 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐹 𝑥 = ( 𝑧 ∩ 𝐴 ) ) )
40 vex ⊢ 𝑤 ∈ V
41 40 inex1 ⊢ ( 𝑤 ∩ 𝐴 ) ∈ V
42 41 a1i ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 = ( 𝑧 ∩ 𝐴 ) ) ∧ 𝑤 ∈ 𝐹 ) → ( 𝑤 ∩ 𝐴 ) ∈ V )
43 elrest ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ∈ V ) → ( 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ↔ ∃ 𝑤 ∈ 𝐹 𝑦 = ( 𝑤 ∩ 𝐴 ) ) )
44 4 43 syldan ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ↔ ∃ 𝑤 ∈ 𝐹 𝑦 = ( 𝑤 ∩ 𝐴 ) ) )
45 44 adantr ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 = ( 𝑧 ∩ 𝐴 ) ) → ( 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ↔ ∃ 𝑤 ∈ 𝐹 𝑦 = ( 𝑤 ∩ 𝐴 ) ) )
46 ineq12 ⊢ ( ( 𝑥 = ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑤 ∩ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) = ( ( 𝑧 ∩ 𝐴 ) ∩ ( 𝑤 ∩ 𝐴 ) ) )
47 inindir ⊢ ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) = ( ( 𝑧 ∩ 𝐴 ) ∩ ( 𝑤 ∩ 𝐴 ) )
48 46 47 eqtr4di ⊢ ( ( 𝑥 = ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑤 ∩ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) = ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) )
49 48 pweqd ⊢ ( ( 𝑥 = ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑤 ∩ 𝐴 ) ) → 𝒫 ( 𝑥 ∩ 𝑦 ) = 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) )
50 49 ineq2d ⊢ ( ( 𝑥 = ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑤 ∩ 𝐴 ) ) → ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) = ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ) )
51 50 neeq1d ⊢ ( ( 𝑥 = ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑤 ∩ 𝐴 ) ) → ( ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ) ≠ ∅ ) )
52 51 adantll ⊢ ( ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 = ( 𝑧 ∩ 𝐴 ) ) ∧ 𝑦 = ( 𝑤 ∩ 𝐴 ) ) → ( ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ) ≠ ∅ ) )
53 42 45 52 ralxfr2d ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 = ( 𝑧 ∩ 𝐴 ) ) → ( ∀ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∀ 𝑤 ∈ 𝐹 ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ) ≠ ∅ ) )
54 37 39 53 ralxfr2d ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∀ 𝑥 ∈ ( 𝐹 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ↔ ∀ 𝑧 ∈ 𝐹 ∀ 𝑤 ∈ 𝐹 ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( ( 𝑧 ∩ 𝑤 ) ∩ 𝐴 ) ) ≠ ∅ ) )
55 34 54 mpbird ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ∀ 𝑥 ∈ ( 𝐹 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ )
56 isfbas ⊢ ( 𝐴 ∈ V → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ( ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ∧ ( ( 𝐹 ↾t 𝐴 ) ≠ ∅ ∧ ∅ ∉ ( 𝐹 ↾t 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝐹 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
57 56 baibd ⊢ ( ( 𝐴 ∈ V ∧ ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ( ( 𝐹 ↾t 𝐴 ) ≠ ∅ ∧ ∅ ∉ ( 𝐹 ↾t 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝐹 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) )
58 3anan32 ⊢ ( ( ( 𝐹 ↾t 𝐴 ) ≠ ∅ ∧ ∅ ∉ ( 𝐹 ↾t 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝐹 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ↔ ( ( ( 𝐹 ↾t 𝐴 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐹 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ∧ ∅ ∉ ( 𝐹 ↾t 𝐴 ) ) )
59 57 58 bitrdi ⊢ ( ( 𝐴 ∈ V ∧ ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ( ( ( 𝐹 ↾t 𝐴 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐹 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ∧ ∅ ∉ ( 𝐹 ↾t 𝐴 ) ) ) )
60 59 baibd ⊢ ( ( ( 𝐴 ∈ V ∧ ( 𝐹 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ) ∧ ( ( 𝐹 ↾t 𝐴 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐹 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐹 ↾t 𝐴 ) ( ( 𝐹 ↾t 𝐴 ) ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ∅ ∉ ( 𝐹 ↾t 𝐴 ) ) )
61 4 6 17 55 60 syl22anc ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ∅ ∉ ( 𝐹 ↾t 𝐴 ) ) )
62 df-nel ⊢ ( ∅ ∉ ( 𝐹 ↾t 𝐴 ) ↔ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) )
63 61 62 bitrdi ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) )