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 difexg ⊢ ( 𝑋 ∈ dom card → ( 𝑋 ∖ 𝑤 ) ∈ V )
32 30 31 syl ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( 𝑋 ∖ 𝑤 ) ∈ V )
33 sscon ⊢ ( 𝑤 ⊆ 𝑧 → ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑤 ) )
34 33 3ad2ant3 ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑤 ) )
35 ssdomg ⊢ ( ( 𝑋 ∖ 𝑤 ) ∈ V → ( ( 𝑋 ∖ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑤 ) → ( 𝑋 ∖ 𝑧 ) ≼ ( 𝑋 ∖ 𝑤 ) ) )
36 32 34 35 sylc ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( 𝑋 ∖ 𝑧 ) ≼ ( 𝑋 ∖ 𝑤 ) )
37 domsdomtr ⊢ ( ( ( 𝑋 ∖ 𝑧 ) ≼ ( 𝑋 ∖ 𝑤 ) ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) → ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 )
38 37 ex ⊢ ( ( 𝑋 ∖ 𝑧 ) ≼ ( 𝑋 ∖ 𝑤 ) → ( ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 → ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ) )
39 36 38 syl ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 → ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ) )
40 vex ⊢ 𝑤 ∈ V
41 difeq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ 𝑤 ) )
42 41 breq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) )
43 40 42 sbcie ⊢ ( [ 𝑤 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 )
44 vex ⊢ 𝑧 ∈ V
45 difeq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ 𝑧 ) )
46 45 breq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ) )
47 44 46 sbcie ⊢ ( [ 𝑧 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 )
48 39 43 47 3imtr4g ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑧 ) → ( [ 𝑤 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 → [ 𝑧 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) )
49 infunsdom ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) ) → ( ( 𝑋 ∖ 𝑧 ) ∪ ( 𝑋 ∖ 𝑤 ) ) ≺ 𝑋 )
50 49 ex ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ( ( ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) → ( ( 𝑋 ∖ 𝑧 ) ∪ ( 𝑋 ∖ 𝑤 ) ) ≺ 𝑋 ) )
51 difindi ⊢ ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) = ( ( 𝑋 ∖ 𝑧 ) ∪ ( 𝑋 ∖ 𝑤 ) )
52 51 breq1i ⊢ ( ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) ≺ 𝑋 ↔ ( ( 𝑋 ∖ 𝑧 ) ∪ ( 𝑋 ∖ 𝑤 ) ) ≺ 𝑋 )
53 50 52 syl6ibr ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → ( ( ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) → ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) ≺ 𝑋 ) )
54 53 3ad2ant1 ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋 ) → ( ( ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) → ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) ≺ 𝑋 ) )
55 47 43 anbi12i ⊢ ( ( [ 𝑧 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ∧ [ 𝑤 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) ↔ ( ( 𝑋 ∖ 𝑧 ) ≺ 𝑋 ∧ ( 𝑋 ∖ 𝑤 ) ≺ 𝑋 ) )
56 44 inex1 ⊢ ( 𝑧 ∩ 𝑤 ) ∈ V
57 difeq2 ⊢ ( 𝑦 = ( 𝑧 ∩ 𝑤 ) → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) )
58 57 breq1d ⊢ ( 𝑦 = ( 𝑧 ∩ 𝑤 ) → ( ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) ≺ 𝑋 ) )
59 56 58 sbcie ⊢ ( [ ( 𝑧 ∩ 𝑤 ) / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ ( 𝑧 ∩ 𝑤 ) ) ≺ 𝑋 )
60 54 55 59 3imtr4g ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝑧 ⊆ 𝑋 ∧ 𝑤 ⊆ 𝑋 ) → ( ( [ 𝑧 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ∧ [ 𝑤 / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) → [ ( 𝑧 ∩ 𝑤 ) / 𝑦 ] ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ) )
61 7 8 20 29 48 60 isfild ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ≺ 𝑋 } ∈ ( Fil ‘ 𝑋 ) )