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	syl6eq	$⊢ 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		difexg	$⊢ X \in dom card \to X ∖ w \in V$
32	30 31	syl	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq z) \to X ∖ w \in V$
33		sscon	$⊢ w \subseteq z \to X ∖ z \subseteq X ∖ w$
34	33	3ad2ant3	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq z) \to X ∖ z \subseteq X ∖ w$
35		ssdomg	$⊢ X ∖ w \in V \to (X ∖ z \subseteq X ∖ w \to (X ∖ z) ≼ (X ∖ w))$
36	32 34 35	sylc	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq z) \to (X ∖ z) ≼ (X ∖ w)$
37		domsdomtr	$⊢ ((X ∖ z) ≼ (X ∖ w) \land (X ∖ w) ≺ X) \to (X ∖ z) ≺ X$
38	37	ex	$⊢ (X ∖ z) ≼ (X ∖ w) \to ((X ∖ w) ≺ X \to (X ∖ z) ≺ X)$
39	36 38	syl	$⊢ ((X \in dom card \land ω ≼ X) \land z \subseteq X \land w \subseteq z) \to ((X ∖ w) ≺ X \to (X ∖ z) ≺ X)$
40		vex	$⊢ w \in V$
41		difeq2	$⊢ y = w \to X ∖ y = X ∖ w$
42	41	breq1d	$⊢ y = w \to ((X ∖ y) ≺ X \leftrightarrow (X ∖ w) ≺ X)$
43	40 42	sbcie	$⊢ \underset{˙}{[} w / y \underset{˙}{]} (X ∖ y) ≺ X \leftrightarrow (X ∖ w) ≺ X$
44		vex	$⊢ z \in V$
45		difeq2	$⊢ y = z \to X ∖ y = X ∖ z$
46	45	breq1d	$⊢ y = z \to ((X ∖ y) ≺ X \leftrightarrow (X ∖ z) ≺ X)$
47	44 46	sbcie	$⊢ \underset{˙}{[} z / y \underset{˙}{]} (X ∖ y) ≺ X \leftrightarrow (X ∖ z) ≺ X$
48	39 43 47	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)$
49		infunsdom	$⊢ ((X \in dom card \land ω ≼ X) \land ((X ∖ z) ≺ X \land (X ∖ w) ≺ X)) \to ((X ∖ z) \cup (X ∖ w)) ≺ X$
50	49	ex	$⊢ (X \in dom card \land ω ≼ X) \to (((X ∖ z) ≺ X \land (X ∖ w) ≺ X) \to ((X ∖ z) \cup (X ∖ w)) ≺ X)$
51		difindi	$⊢ X ∖ (z \cap w) = (X ∖ z) \cup (X ∖ w)$
52	51	breq1i	$⊢ (X ∖ (z \cap w)) ≺ X \leftrightarrow ((X ∖ z) \cup (X ∖ w)) ≺ X$
53	50 52	syl6ibr	$⊢ (X \in dom card \land ω ≼ X) \to (((X ∖ z) ≺ X \land (X ∖ w) ≺ X) \to (X ∖ (z \cap w)) ≺ X)$
54	53	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)$
55	47 43	anbi12i	$⊢ (\underset{˙}{[} z / y \underset{˙}{]} (X ∖ y) ≺ X \land \underset{˙}{[} w / y \underset{˙}{]} (X ∖ y) ≺ X) \leftrightarrow ((X ∖ z) ≺ X \land (X ∖ w) ≺ X)$
56	44	inex1	$⊢ z \cap w \in V$
57		difeq2	$⊢ y = z \cap w \to X ∖ y = X ∖ (z \cap w)$
58	57	breq1d	$⊢ y = z \cap w \to ((X ∖ y) ≺ X \leftrightarrow (X ∖ (z \cap w)) ≺ X)$
59	56 58	sbcie	$⊢ \underset{˙}{[} (z \cap w) / y \underset{˙}{]} (X ∖ y) ≺ X \leftrightarrow (X ∖ (z \cap w)) ≺ X$
60	54 55 59	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)$
61	7 8 20 29 48 60	isfild	$⊢ (X \in dom card \land ω ≼ X) \to \{x \in 𝒫 X \| (X ∖ x) ≺ X\} \in Fil (X)$

Metamath Proof Explorer

Theorem csdfil

Proof