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 F fBas Y A Y F 𝑡 A fBas A ¬ F 𝑡 A

Proof

Step Hyp Ref Expression
1 elfvdm F fBas Y Y dom fBas
2 ssexg A Y Y dom fBas A V
3 2 ancoms Y dom fBas A Y A V
4 1 3 sylan F fBas Y A Y A V
5 restsspw F 𝑡 A 𝒫 A
6 5 a1i F fBas Y A Y F 𝑡 A 𝒫 A
7 fbasne0 F fBas Y F
8 7 adantr F fBas Y A Y F
9 n0 F x x F
10 8 9 sylib F fBas Y A Y x x F
11 elrestr F fBas Y A V x F x A F 𝑡 A
12 11 3expia F fBas Y A V x F x A F 𝑡 A
13 4 12 syldan F fBas Y A Y x F x A F 𝑡 A
14 ne0i x A F 𝑡 A F 𝑡 A
15 13 14 syl6 F fBas Y A Y x F F 𝑡 A
16 15 exlimdv F fBas Y A Y x x F F 𝑡 A
17 10 16 mpd F fBas Y A Y F 𝑡 A
18 fbasssin F fBas Y z F w F x F x z w
19 18 3expb F fBas Y z F w F x F x z w
20 19 adantlr F fBas Y A Y z F w F x F x z w
21 simplll F fBas Y A Y z F w F x F x z w F fBas Y
22 4 ad2antrr F fBas Y A Y z F w F x F x z w A V
23 simprl F fBas Y A Y z F w F x F x z w x F
24 21 22 23 11 syl3anc F fBas Y A Y z F w F x F x z w x A F 𝑡 A
25 ssrin x z w x A z w A
26 25 ad2antll F fBas Y A Y z F w F x F x z w x A z w A
27 vex x V
28 27 inex1 x A V
29 28 elpw x A 𝒫 z w A x A z w A
30 26 29 sylibr F fBas Y A Y z F w F x F x z w x A 𝒫 z w A
31 inelcm x A F 𝑡 A x A 𝒫 z w A F 𝑡 A 𝒫 z w A
32 24 30 31 syl2anc F fBas Y A Y z F w F x F x z w F 𝑡 A 𝒫 z w A
33 20 32 rexlimddv F fBas Y A Y z F w F F 𝑡 A 𝒫 z w A
34 33 ralrimivva F fBas Y A Y z F w F F 𝑡 A 𝒫 z w A
35 vex z V
36 35 inex1 z A V
37 36 a1i F fBas Y A Y z F z A V
38 elrest F fBas Y A V x F 𝑡 A z F x = z A
39 4 38 syldan F fBas Y A Y x F 𝑡 A z F x = z A
40 vex w V
41 40 inex1 w A V
42 41 a1i F fBas Y A Y x = z A w F w A V
43 elrest F fBas Y A V y F 𝑡 A w F y = w A
44 4 43 syldan F fBas Y A Y y F 𝑡 A w F y = w A
45 44 adantr F fBas Y A Y x = z A y F 𝑡 A w F y = w A
46 ineq12 x = z A y = w A x y = z A w A
47 inindir z w A = z A w A
48 46 47 eqtr4di x = z A y = w A x y = z w A
49 48 pweqd x = z A y = w A 𝒫 x y = 𝒫 z w A
50 49 ineq2d x = z A y = w A F 𝑡 A 𝒫 x y = F 𝑡 A 𝒫 z w A
51 50 neeq1d x = z A y = w A F 𝑡 A 𝒫 x y F 𝑡 A 𝒫 z w A
52 51 adantll F fBas Y A Y x = z A y = w A F 𝑡 A 𝒫 x y F 𝑡 A 𝒫 z w A
53 42 45 52 ralxfr2d F fBas Y A Y x = z A y F 𝑡 A F 𝑡 A 𝒫 x y w F F 𝑡 A 𝒫 z w A
54 37 39 53 ralxfr2d F fBas Y A Y x F 𝑡 A y F 𝑡 A F 𝑡 A 𝒫 x y z F w F F 𝑡 A 𝒫 z w A
55 34 54 mpbird F fBas Y A Y x F 𝑡 A y F 𝑡 A F 𝑡 A 𝒫 x y
56 isfbas A V F 𝑡 A fBas A F 𝑡 A 𝒫 A F 𝑡 A F 𝑡 A x F 𝑡 A y F 𝑡 A F 𝑡 A 𝒫 x y
57 56 baibd A V F 𝑡 A 𝒫 A F 𝑡 A fBas A F 𝑡 A F 𝑡 A x F 𝑡 A y F 𝑡 A F 𝑡 A 𝒫 x y
58 3anan32 F 𝑡 A F 𝑡 A x F 𝑡 A y F 𝑡 A F 𝑡 A 𝒫 x y F 𝑡 A x F 𝑡 A y F 𝑡 A F 𝑡 A 𝒫 x y F 𝑡 A
59 57 58 bitrdi A V F 𝑡 A 𝒫 A F 𝑡 A fBas A F 𝑡 A x F 𝑡 A y F 𝑡 A F 𝑡 A 𝒫 x y F 𝑡 A
60 59 baibd A V F 𝑡 A 𝒫 A F 𝑡 A x F 𝑡 A y F 𝑡 A F 𝑡 A 𝒫 x y F 𝑡 A fBas A F 𝑡 A
61 4 6 17 55 60 syl22anc F fBas Y A Y F 𝑡 A fBas A F 𝑡 A
62 df-nel F 𝑡 A ¬ F 𝑡 A
63 61 62 bitrdi F fBas Y A Y F 𝑡 A fBas A ¬ F 𝑡 A