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	$⊢ (X \in dom card \land ω ≼ X) \to \{x \in 𝒫 X \| (X ∖ x) ≺ X\} \in Fil (X)$

Proof

Step	Hyp	Ref	Expression
1		difeq2	$⊢ x = y \to X ∖ x = X ∖ y$
2	1	breq1d	$⊢ x = y \to ((X ∖ x) ≺ X \leftrightarrow (X ∖ y) ≺ X)$
3	2	elrab	$⊢ y \in \{x \in 𝒫 X \| (X ∖ x) ≺ X\} \leftrightarrow (y \in 𝒫 X \land (X ∖ y) ≺ X)$
4		velpw	$⊢ y \in 𝒫 X \leftrightarrow y \subseteq X$
5	4	anbi1i	$⊢ (y \in 𝒫 X \land (X ∖ y) ≺ X) \leftrightarrow (y \subseteq X \land (X ∖ y) ≺ X)$
6	3 5	bitri	$⊢ y \in \{x \in 𝒫 X \| (X ∖ x) ≺ X\} \leftrightarrow (y \subseteq X \land (X ∖ y) ≺ X)$
7	6	a1i	$⊢ (X \in dom card \land ω ≼ X) \to (y \in \{x \in 𝒫 X \| (X ∖ x) ≺ X\} \leftrightarrow (y \subseteq X \land (X ∖ y) ≺ X))$
8		simpl	$⊢ (X \in dom card \land ω ≼ X) \to X \in dom card$
9		difid	$⊢ X ∖ X = \emptyset$
10		infn0	$⊢ ω ≼ X \to X \neq \emptyset$
11	10	adantl	$⊢ (X \in dom card \land ω ≼ X) \to X \neq \emptyset$
12		0sdomg	$⊢ X \in dom card \to (\emptyset ≺ X \leftrightarrow X \neq \emptyset)$
13	12	adantr	$⊢ (X \in dom card \land ω ≼ X) \to (\emptyset ≺ X \leftrightarrow X \neq \emptyset)$
14	11 13	mpbird	$⊢ (X \in dom card \land ω ≼ X) \to \emptyset ≺ X$
15	9 14	eqbrtrid	$⊢ (X \in dom card \land ω ≼ X) \to (X ∖ X) ≺ X$
16		difeq2	$⊢ y = X \to X ∖ y = X ∖ X$
17	16	breq1d	$⊢ y = X \to ((X ∖ y) ≺ X \leftrightarrow (X ∖ X) ≺ X)$
18	17	sbcieg	$⊢ X \in dom card \to (\underset{˙}{[} X / y \underset{˙}{]} (X ∖ y) ≺ X \leftrightarrow (X ∖ X) ≺ X)$
19	18	adantr	$⊢ (X \in dom card \land ω ≼ X) \to (\underset{˙}{[} X / y \underset{˙}{]} (X ∖ y) ≺ X \leftrightarrow (X ∖ X) ≺ X)$
20	15 19	mpbird	$⊢ (X \in dom card \land ω ≼ X) \to \underset{˙}{[} X / y \underset{˙}{]} (X ∖ y) ≺ X$
21		sdomirr	$⊢ \neg X ≺ X$
22		0ex	$⊢ \emptyset \in V$
23		difeq2	$⊢ y = \emptyset \to X ∖ y = X ∖ \emptyset$
24		dif0	$⊢ X ∖ \emptyset = X$
25	23 24	eqtrdi	$⊢ y = \emptyset \to X ∖ y = X$
26	25	breq1d	$⊢ y = \emptyset \to ((X ∖ y) ≺ X \leftrightarrow X ≺ X)$
27	22 26	sbcie	$⊢ \underset{˙}{[} \emptyset / y \underset{˙}{]} (X ∖ y) ≺ X \leftrightarrow X ≺ X$
28	27	a1i	$⊢ (X \in dom card \land ω ≼ X) \to (\underset{˙}{[} \emptyset / y \underset{˙}{]} (X ∖ y) ≺ X \leftrightarrow X ≺ X)$
29	21 28	mtbiri	$⊢ (X \in dom card \land ω ≼ X) \to \neg \underset{˙}{[} \emptyset / y \underset{˙}{]} (X ∖ y) ≺ X$
30		simp1l	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq z) \to X \in dom card$
31	30	difexd	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq z) \to X ∖ w \in V$
32		sscon	$⊢ w \subseteq z \to X ∖ z \subseteq X ∖ w$
33	32	3ad2ant3	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq z) \to X ∖ z \subseteq X ∖ w$
34		ssdomg	$⊢ X ∖ w \in V \to (X ∖ z \subseteq X ∖ w \to (X ∖ z) ≼ (X ∖ w))$
35	31 33 34	sylc	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq z) \to (X ∖ z) ≼ (X ∖ w)$
36		domsdomtr	$⊢ ((X ∖ z) ≼ (X ∖ w) \land (X ∖ w) ≺ X) \to (X ∖ z) ≺ X$
37	36	ex	$⊢ (X ∖ z) ≼ (X ∖ w) \to ((X ∖ w) ≺ X \to (X ∖ z) ≺ X)$
38	35 37	syl	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq z) \to ((X ∖ w) ≺ X \to (X ∖ z) ≺ X)$
39		vex	$⊢ w \in V$
40		difeq2	$⊢ y = w \to X ∖ y = X ∖ w$
41	40	breq1d	$⊢ y = w \to ((X ∖ y) ≺ X \leftrightarrow (X ∖ w) ≺ X)$
42	39 41	sbcie	$⊢ \underset{˙}{[} w / y \underset{˙}{]} (X ∖ y) ≺ X \leftrightarrow (X ∖ w) ≺ X$
43		vex	$⊢ z \in V$
44		difeq2	$⊢ y = z \to X ∖ y = X ∖ z$
45	44	breq1d	$⊢ y = z \to ((X ∖ y) ≺ X \leftrightarrow (X ∖ z) ≺ X)$
46	43 45	sbcie	$⊢ \underset{˙}{[} z / y \underset{˙}{]} (X ∖ y) ≺ X \leftrightarrow (X ∖ z) ≺ X$
47	38 42 46	3imtr4g	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq z) \to (\underset{˙}{[} w / y \underset{˙}{]} (X ∖ y) ≺ X \to \underset{˙}{[} z / y \underset{˙}{]} (X ∖ y) ≺ X)$
48		infunsdom	$⊢ ((X \in dom card \land ω ≼ X) \land ((X ∖ z) ≺ X \land (X ∖ w) ≺ X)) \to ((X ∖ z) \cup (X ∖ w)) ≺ X$
49	48	ex	$⊢ (X \in dom card \land ω ≼ X) \to (((X ∖ z) ≺ X \land (X ∖ w) ≺ X) \to ((X ∖ z) \cup (X ∖ w)) ≺ X)$
50		difindi	$⊢ X ∖ (z \cap w) = (X ∖ z) \cup (X ∖ w)$
51	50	breq1i	$⊢ (X ∖ (z \cap w)) ≺ X \leftrightarrow ((X ∖ z) \cup (X ∖ w)) ≺ X$
52	49 51	syl6ibr	$⊢ (X \in dom card \land ω ≼ X) \to (((X ∖ z) ≺ X \land (X ∖ w) ≺ X) \to (X ∖ (z \cap w)) ≺ X)$
53	52	3ad2ant1	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq X) \to (((X ∖ z) ≺ X \land (X ∖ w) ≺ X) \to (X ∖ (z \cap w)) ≺ X)$
54	46 42	anbi12i	$⊢ (\underset{˙}{[} z / y \underset{˙}{]} (X ∖ y) ≺ X \land \underset{˙}{[} w / y \underset{˙}{]} (X ∖ y) ≺ X) \leftrightarrow ((X ∖ z) ≺ X \land (X ∖ w) ≺ X)$
55	43	inex1	$⊢ z \cap w \in V$
56		difeq2	$⊢ y = z \cap w \to X ∖ y = X ∖ (z \cap w)$
57	56	breq1d	$⊢ y = z \cap w \to ((X ∖ y) ≺ X \leftrightarrow (X ∖ (z \cap w)) ≺ X)$
58	55 57	sbcie	$⊢ \underset{˙}{[} (z \cap w) / y \underset{˙}{]} (X ∖ y) ≺ X \leftrightarrow (X ∖ (z \cap w)) ≺ X$
59	53 54 58	3imtr4g	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq X) \to ((\underset{˙}{[} z / y \underset{˙}{]} (X ∖ y) ≺ X \land \underset{˙}{[} w / y \underset{˙}{]} (X ∖ y) ≺ X) \to \underset{˙}{[} (z \cap w) / y \underset{˙}{]} (X ∖ y) ≺ X)$
60	7 8 20 29 47 59	isfild	$⊢ (X \in dom card \land ω ≼ X) \to \{x \in 𝒫 X \| (X ∖ x) ≺ X\} \in Fil (X)$

Metamath Proof Explorer

Theorem csdfil

Proof