Metamath Proof Explorer

Theorem csdfil

Description: The set of all elements whose complement is dominated by the base set is a filter. (Contributed by Mario Carneiro, 14-Dec-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion csdfil ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ≺ 𝑋 } ∈ ( Fil ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 difeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑋 ∖ 𝑥 ) = ( 𝑋 ∖ 𝑦 ) )
2 1 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑋 ∖ 𝑥 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) )
3 2 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ≺ 𝑋 } ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) )
4 velpw ⊢ ( 𝑦 ∈ 𝒫 𝑋 ↔ 𝑦 ⊆ 𝑋 )
5 4 anbi1i ⊢ ( ( 𝑦 ∈ 𝒫 𝑋 ∧ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) ↔ ( 𝑦 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) )
6 3 5 bitri ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ≺ 𝑋 } ↔ ( 𝑦 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) )
7 6 a1i ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ≺ 𝑋 } ↔ ( 𝑦 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) ) )
8 simpl ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → 𝑋 ∈ dom card )
9 difid ⊢ ( 𝑋 ∖ 𝑋 ) = ∅
10 infn0 ⊢ ( ω ≼ 𝑋 → 𝑋 ≠ ∅ )
11 10 adantl ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → 𝑋 ≠ ∅ )
12 0sdomg ⊢ ( 𝑋 ∈ dom card → ( ∅ ≺ 𝑋 ↔ 𝑋 ≠ ∅ ) )
13 12 adantr ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ( ∅ ≺ 𝑋 ↔ 𝑋 ≠ ∅ ) )
14 11 13 mpbird ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ∅ ≺ 𝑋 )
15 9 14 eqbrtrid ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ( 𝑋 ∖ 𝑋 ) ≺ 𝑋 )
16 difeq2 ⊢ ( 𝑦 = 𝑋 → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ 𝑋 ) )
17 16 breq1d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑋 ) ≺ 𝑋 ) )
18 17 sbcieg ⊢ ( 𝑋 ∈ dom card → ( [ 𝑋 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑋 ) ≺ 𝑋 ) )
19 18 adantr ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ( [ 𝑋 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑋 ) ≺ 𝑋 ) )
20 15 19 mpbird ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → [ 𝑋 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 )
21 sdomirr ⊢ ¬ 𝑋 ≺ 𝑋
22 0ex ⊢ ∅ ∈ V
23 difeq2 ⊢ ( 𝑦 = ∅ → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ ∅ ) )
24 dif0 ⊢ ( 𝑋 ∖ ∅ ) = 𝑋
25 23 24 eqtrdi ⊢ ( 𝑦 = ∅ → ( 𝑋 ∖ 𝑦 ) = 𝑋 )
26 25 breq1d ⊢ ( 𝑦 = ∅ → ( ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋 ) )
27 22 26 sbcie ⊢ ( [ ∅ / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋 )
28 27 a1i ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ( [ ∅ / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ 𝑋 ≺ 𝑋 ) )
29 21 28 mtbiri ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ¬ [ ∅ / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 )
30 simp1l ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → 𝑋 ∈ dom card )
31 30 difexd ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( 𝑋 ∖ 𝑤 ) ∈ V )
32 sscon ⊢ ( 𝑤 ⊆ 𝑧 → ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑤 ) )
33 32 3ad2ant3 ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑤 ) )
34 ssdomg ⊢ ( ( 𝑋 ∖ 𝑤 ) ∈ V → ( ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑤 ) → ( 𝑋 ∖ 𝑧 ) ≼ ( 𝑋 ∖ 𝑤 ) ) )
35 31 33 34 sylc ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( 𝑋 ∖ 𝑧 ) ≼ ( 𝑋 ∖ 𝑤 ) )
36 domsdomtr ⊢ ( ( ( 𝑋 ∖ 𝑧 ) ≼ ( 𝑋 ∖ 𝑤 ) ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) → ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 )
37 36 ex ⊢ ( ( 𝑋 ∖ 𝑧 ) ≼ ( 𝑋 ∖ 𝑤 ) → ( ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 → ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ) )
38 35 37 syl ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 → ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ) )
39 vex ⊢ 𝑤 ∈ V
40 difeq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ 𝑤 ) )
41 40 breq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) )
42 39 41 sbcie ⊢ ( [ 𝑤 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 )
43 vex ⊢ 𝑧 ∈ V
44 difeq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ 𝑧 ) )
45 44 breq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ) )
46 43 45 sbcie ⊢ ( [ 𝑧 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 )
47 38 42 46 3imtr4g ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( [ 𝑤 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 → [ 𝑧 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) )
48 infunsdom ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) ) → ( ( 𝑋 ∖ 𝑧 ) ∪ ( 𝑋 ∖ 𝑤 ) ) ≺ 𝑋 )
49 48 ex ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ( ( ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) → ( ( 𝑋 ∖ 𝑧 ) ∪ ( 𝑋 ∖ 𝑤 ) ) ≺ 𝑋 ) )
50 difindi ⊢ ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) = ( ( 𝑋 ∖ 𝑧 ) ∪ ( 𝑋 ∖ 𝑤 ) )
51 50 breq1i ⊢ ( ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) ≺ 𝑋 ↔ ( ( 𝑋 ∖ 𝑧 ) ∪ ( 𝑋 ∖ 𝑤 ) ) ≺ 𝑋 )
52 49 51 syl6ibr ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ( ( ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) → ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) ≺ 𝑋 ) )
53 52 3ad2ant1 ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋 ) → ( ( ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) → ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) ≺ 𝑋 ) )
54 46 42 anbi12i ⊢ ( ( [ 𝑧 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ∧ [ 𝑤 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) ↔ ( ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) )
55 43 inex1 ⊢ ( 𝑧 ∩ 𝑤 ) ∈ V
56 difeq2 ⊢ ( 𝑦 = ( 𝑧 ∩ 𝑤 ) → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) )
57 56 breq1d ⊢ ( 𝑦 = ( 𝑧 ∩ 𝑤 ) → ( ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) ≺ 𝑋 ) )
58 55 57 sbcie ⊢ ( [ ( 𝑧 ∩ 𝑤 ) / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) ≺ 𝑋 )
59 53 54 58 3imtr4g ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋 ) → ( ( [ 𝑧 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ∧ [ 𝑤 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) → [ ( 𝑧 ∩ 𝑤 ) / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) )
60 7 8 20 29 47 59 isfild ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ≺ 𝑋 } ∈ ( Fil ‘ 𝑋 ) )