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	syl5bb	⊢ ( ( 𝐿 ∈ ( 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	syl5bb	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∀ 𝑣 ∈ 𝐿 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )
16	1 15	bitrd	⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ¬ ( 𝑌 ∖ 𝐴 ) ∈ 𝐿 ) )