isf34lem4

		Ref	Expression
	Hypothesis	compss.a	$⊢ F = (x \in 𝒫 A ⟼ A ∖ x)$
	Assertion	isf34lem4	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F (⋃ X) = ⋂ F [X]$

Proof

Step	Hyp	Ref	Expression
1		compss.a	$⊢ F = (x \in 𝒫 A ⟼ A ∖ x)$
2		sspwuni	$⊢ X \subseteq 𝒫 A \leftrightarrow ⋃ X \subseteq A$
3	1	isf34lem1	$⊢ (A \in V \land ⋃ X \subseteq A) \to F (⋃ X) = A ∖ ⋃ X$
4	2 3	sylan2b	$⊢ (A \in V \land X \subseteq 𝒫 A) \to F (⋃ X) = A ∖ ⋃ X$
5	4	adantrr	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F (⋃ X) = A ∖ ⋃ X$
6		simplrr	$⊢ (((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \land (a \in 𝒫 A \land A ∖ a \in X)) \to \neg b \in ⋃ X$
7		simprl	$⊢ ((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \to b \in A$
8	7	ad2antrr	$⊢ ((((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \land (a \in 𝒫 A \land A ∖ a \in X)) \land \neg b \in a) \to b \in A$
9		simpr	$⊢ ((((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \land (a \in 𝒫 A \land A ∖ a \in X)) \land \neg b \in a) \to \neg b \in a$
10	8 9	eldifd	$⊢ ((((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \land (a \in 𝒫 A \land A ∖ a \in X)) \land \neg b \in a) \to b \in (A ∖ a)$
11		simplrr	$⊢ ((((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \land (a \in 𝒫 A \land A ∖ a \in X)) \land \neg b \in a) \to A ∖ a \in X$
12		elunii	$⊢ (b \in (A ∖ a) \land A ∖ a \in X) \to b \in ⋃ X$
13	10 11 12	syl2anc	$⊢ ((((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \land (a \in 𝒫 A \land A ∖ a \in X)) \land \neg b \in a) \to b \in ⋃ X$
14	13	ex	$⊢ (((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \land (a \in 𝒫 A \land A ∖ a \in X)) \to (\neg b \in a \to b \in ⋃ X)$
15	6 14	mt3d	$⊢ (((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \land (a \in 𝒫 A \land A ∖ a \in X)) \to b \in a$
16	15	expr	$⊢ (((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \land a \in 𝒫 A) \to (A ∖ a \in X \to b \in a)$
17	16	ralrimiva	$⊢ ((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in A \land \neg b \in ⋃ X)) \to \forall a \in 𝒫 A (A ∖ a \in X \to b \in a)$
18	17	ex	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to ((b \in A \land \neg b \in ⋃ X) \to \forall a \in 𝒫 A (A ∖ a \in X \to b \in a))$
19		n0	$⊢ X \neq \emptyset \leftrightarrow \exists c c \in X$
20		simpr	$⊢ (A \in V \land X \subseteq 𝒫 A) \to X \subseteq 𝒫 A$
21	20	sselda	$⊢ ((A \in V \land X \subseteq 𝒫 A) \land c \in X) \to c \in 𝒫 A$
22	21	elpwid	$⊢ ((A \in V \land X \subseteq 𝒫 A) \land c \in X) \to c \subseteq A$
23		dfss4	$⊢ c \subseteq A \leftrightarrow A ∖ (A ∖ c) = c$
24	22 23	sylib	$⊢ ((A \in V \land X \subseteq 𝒫 A) \land c \in X) \to A ∖ (A ∖ c) = c$
25		simpr	$⊢ ((A \in V \land X \subseteq 𝒫 A) \land c \in X) \to c \in X$
26	24 25	eqeltrd	$⊢ ((A \in V \land X \subseteq 𝒫 A) \land c \in X) \to A ∖ (A ∖ c) \in X$
27		difss	$⊢ A ∖ c \subseteq A$
28		elpw2g	$⊢ A \in V \to (A ∖ c \in 𝒫 A \leftrightarrow A ∖ c \subseteq A)$
29	27 28	mpbiri	$⊢ A \in V \to A ∖ c \in 𝒫 A$
30	29	ad2antrr	$⊢ ((A \in V \land X \subseteq 𝒫 A) \land c \in X) \to A ∖ c \in 𝒫 A$
31		difeq2	$⊢ a = A ∖ c \to A ∖ a = A ∖ (A ∖ c)$
32	31	eleq1d	$⊢ a = A ∖ c \to (A ∖ a \in X \leftrightarrow A ∖ (A ∖ c) \in X)$
33		eleq2	$⊢ a = A ∖ c \to (b \in a \leftrightarrow b \in (A ∖ c))$
34	32 33	imbi12d	$⊢ a = A ∖ c \to ((A ∖ a \in X \to b \in a) \leftrightarrow (A ∖ (A ∖ c) \in X \to b \in (A ∖ c)))$
35	34	rspcv	$⊢ A ∖ c \in 𝒫 A \to (\forall a \in 𝒫 A (A ∖ a \in X \to b \in a) \to (A ∖ (A ∖ c) \in X \to b \in (A ∖ c)))$
36	30 35	syl	$⊢ ((A \in V \land X \subseteq 𝒫 A) \land c \in X) \to (\forall a \in 𝒫 A (A ∖ a \in X \to b \in a) \to (A ∖ (A ∖ c) \in X \to b \in (A ∖ c)))$
37	26 36	mpid	$⊢ ((A \in V \land X \subseteq 𝒫 A) \land c \in X) \to (\forall a \in 𝒫 A (A ∖ a \in X \to b \in a) \to b \in (A ∖ c))$
38		eldifi	$⊢ b \in (A ∖ c) \to b \in A$
39	37 38	syl6	$⊢ ((A \in V \land X \subseteq 𝒫 A) \land c \in X) \to (\forall a \in 𝒫 A (A ∖ a \in X \to b \in a) \to b \in A)$
40	39	ex	$⊢ (A \in V \land X \subseteq 𝒫 A) \to (c \in X \to (\forall a \in 𝒫 A (A ∖ a \in X \to b \in a) \to b \in A))$
41	40	exlimdv	$⊢ (A \in V \land X \subseteq 𝒫 A) \to (\exists c c \in X \to (\forall a \in 𝒫 A (A ∖ a \in X \to b \in a) \to b \in A))$
42	19 41	syl5bi	$⊢ (A \in V \land X \subseteq 𝒫 A) \to (X \neq \emptyset \to (\forall a \in 𝒫 A (A ∖ a \in X \to b \in a) \to b \in A))$
43	42	impr	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to (\forall a \in 𝒫 A (A ∖ a \in X \to b \in a) \to b \in A)$
44		eluni	$⊢ b \in ⋃ X \leftrightarrow \exists c (b \in c \land c \in X)$
45	29	ad2antrr	$⊢ ((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in c \land c \in X)) \to A ∖ c \in 𝒫 A$
46	26	adantlrr	$⊢ ((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land c \in X) \to A ∖ (A ∖ c) \in X$
47	46	adantrl	$⊢ ((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in c \land c \in X)) \to A ∖ (A ∖ c) \in X$
48		elndif	$⊢ b \in c \to \neg b \in (A ∖ c)$
49	48	ad2antrl	$⊢ ((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in c \land c \in X)) \to \neg b \in (A ∖ c)$
50	47 49	jcnd	$⊢ ((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in c \land c \in X)) \to \neg (A ∖ (A ∖ c) \in X \to b \in (A ∖ c))$
51	34	notbid	$⊢ a = A ∖ c \to (\neg (A ∖ a \in X \to b \in a) \leftrightarrow \neg (A ∖ (A ∖ c) \in X \to b \in (A ∖ c)))$
52	51	rspcev	$⊢ (A ∖ c \in 𝒫 A \land \neg (A ∖ (A ∖ c) \in X \to b \in (A ∖ c))) \to \exists a \in 𝒫 A \neg (A ∖ a \in X \to b \in a)$
53	45 50 52	syl2anc	$⊢ ((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in c \land c \in X)) \to \exists a \in 𝒫 A \neg (A ∖ a \in X \to b \in a)$
54		rexnal	$⊢ \exists a \in 𝒫 A \neg (A ∖ a \in X \to b \in a) \leftrightarrow \neg \forall a \in 𝒫 A (A ∖ a \in X \to b \in a)$
55	53 54	sylib	$⊢ ((A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \land (b \in c \land c \in X)) \to \neg \forall a \in 𝒫 A (A ∖ a \in X \to b \in a)$
56	55	ex	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to ((b \in c \land c \in X) \to \neg \forall a \in 𝒫 A (A ∖ a \in X \to b \in a))$
57	56	exlimdv	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to (\exists c (b \in c \land c \in X) \to \neg \forall a \in 𝒫 A (A ∖ a \in X \to b \in a))$
58	44 57	syl5bi	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to (b \in ⋃ X \to \neg \forall a \in 𝒫 A (A ∖ a \in X \to b \in a))$
59	58	con2d	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to (\forall a \in 𝒫 A (A ∖ a \in X \to b \in a) \to \neg b \in ⋃ X)$
60	43 59	jcad	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to (\forall a \in 𝒫 A (A ∖ a \in X \to b \in a) \to (b \in A \land \neg b \in ⋃ X))$
61	18 60	impbid	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to ((b \in A \land \neg b \in ⋃ X) \leftrightarrow \forall a \in 𝒫 A (A ∖ a \in X \to b \in a))$
62		eldif	$⊢ b \in (A ∖ ⋃ X) \leftrightarrow (b \in A \land \neg b \in ⋃ X)$
63		vex	$⊢ b \in V$
64	63	elintrab	$⊢ b \in ⋂ \{a \in 𝒫 A \| A ∖ a \in X\} \leftrightarrow \forall a \in 𝒫 A (A ∖ a \in X \to b \in a)$
65	61 62 64	3bitr4g	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to (b \in (A ∖ ⋃ X) \leftrightarrow b \in ⋂ \{a \in 𝒫 A \| A ∖ a \in X\})$
66	65	eqrdv	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to A ∖ ⋃ X = ⋂ \{a \in 𝒫 A \| A ∖ a \in X\}$
67	5 66	eqtrd	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F (⋃ X) = ⋂ \{a \in 𝒫 A \| A ∖ a \in X\}$
68	1	compss	$⊢ F [X] = \{a \in 𝒫 A \| A ∖ a \in X\}$
69	68	inteqi	$⊢ ⋂ F [X] = ⋂ \{a \in 𝒫 A \| A ∖ a \in X\}$
70	67 69	syl6eqr	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F (⋃ X) = ⋂ F [X]$

Metamath Proof Explorer

Theorem isf34lem4

Proof