This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trfil3

Description: Conditions for the trace of a filter L to be a filter. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion trfil3 ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )

Proof

Step Hyp Ref Expression
1 trfil2 ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ∀ 𝑣 ∈ 𝐿 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ) )
2 dfral2 ⊢ ( ∀ 𝑣 ∈ 𝐿 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ¬ ∃ 𝑣 ∈ 𝐿 ¬ ( 𝑣 ∩ 𝐴 ) ≠ ∅ )
3 nne ⊢ ( ¬ ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ( 𝑣 ∩ 𝐴 ) = ∅ )
4 filelss ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝑣 ∈ 𝐿 ) → 𝑣 ⊆ 𝑌 )
5 reldisj ⊢ ( 𝑣 ⊆ 𝑌 → ( ( 𝑣 ∩ 𝐴 ) = ∅ ↔ 𝑣 ⊆ ( 𝑌 ∖ 𝐴 ) ) )
6 4 5 syl ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝑣 ∈ 𝐿 ) → ( ( 𝑣 ∩ 𝐴 ) = ∅ ↔ 𝑣 ⊆ ( 𝑌 ∖ 𝐴 ) ) )
7 3 6 bitrid ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝑣 ∈ 𝐿 ) → ( ¬ ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ 𝑣 ⊆ ( 𝑌 ∖ 𝐴 ) ) )
8 7 rexbidva ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → ( ∃ 𝑣 ∈ 𝐿 ¬ ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ∃ 𝑣 ∈ 𝐿 𝑣 ⊆ ( 𝑌 ∖ 𝐴 ) ) )
9 8 adantr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∃ 𝑣 ∈ 𝐿 ¬ ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ∃ 𝑣 ∈ 𝐿 𝑣 ⊆ ( 𝑌 ∖ 𝐴 ) ) )
10 difssd ⊢ ( 𝐴 ⊆ 𝑌 → ( 𝑌 ∖ 𝐴 ) ⊆ 𝑌 )
11 elfilss ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝑌 ∖ 𝐴 ) ⊆ 𝑌 ) → ( ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ↔ ∃ 𝑣 ∈ 𝐿 𝑣 ⊆ ( 𝑌 ∖ 𝐴 ) ) )
12 10 11 sylan2 ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ↔ ∃ 𝑣 ∈ 𝐿 𝑣 ⊆ ( 𝑌 ∖ 𝐴 ) ) )
13 9 12 bitr4d ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∃ 𝑣 ∈ 𝐿 ¬ ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )
14 13 notbid ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ¬ ∃ 𝑣 ∈ 𝐿 ¬ ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )
15 2 14 bitrid ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∀ 𝑣 ∈ 𝐿 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )
16 1 15 bitrd ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )