isf34lem5

		Ref	Expression
	Hypothesis	compss.a	$⊢ F = (x \in 𝒫 A ⟼ A ∖ x)$
	Assertion	isf34lem5	$⊢ (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		imassrn	$⊢ F [X] \subseteq ran F$
3	1	isf34lem2	$⊢ A \in V \to F : 𝒫 A ⟶ 𝒫 A$
4	3	adantr	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F : 𝒫 A ⟶ 𝒫 A$
5	4	frnd	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to ran F \subseteq 𝒫 A$
6	2 5	sstrid	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F [X] \subseteq 𝒫 A$
7		simprl	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to X \subseteq 𝒫 A$
8	4	fdmd	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to dom F = 𝒫 A$
9	7 8	sseqtrrd	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to X \subseteq dom F$
10		sseqin2	$⊢ X \subseteq dom F \leftrightarrow dom F \cap X = X$
11	9 10	sylib	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to dom F \cap X = X$
12		simprr	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to X \neq \emptyset$
13	11 12	eqnetrd	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to dom F \cap X \neq \emptyset$
14		imadisj	$⊢ F [X] = \emptyset \leftrightarrow dom F \cap X = \emptyset$
15	14	necon3bii	$⊢ F [X] \neq \emptyset \leftrightarrow dom F \cap X \neq \emptyset$
16	13 15	sylibr	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F [X] \neq \emptyset$
17	6 16	jca	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to (F [X] \subseteq 𝒫 A \land F [X] \neq \emptyset)$
18	1	isf34lem4	$⊢ (A \in V \land (F [X] \subseteq 𝒫 A \land F [X] \neq \emptyset)) \to F (⋃ F [X]) = ⋂ F [F [X]]$
19	17 18	syldan	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F (⋃ F [X]) = ⋂ F [F [X]]$
20	1	isf34lem3	$⊢ (A \in V \land X \subseteq 𝒫 A) \to F [F [X]] = X$
21	20	adantrr	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F [F [X]] = X$
22	21	inteqd	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to ⋂ F [F [X]] = ⋂ X$
23	19 22	eqtrd	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F (⋃ F [X]) = ⋂ X$
24	23	fveq2d	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F (F (⋃ F [X])) = F (⋂ X)$
25	1	compsscnv	$⊢ F^{-1} = F$
26	25	fveq1i	$⊢ F^{-1} (F (⋃ F [X])) = F (F (⋃ F [X]))$
27	1	compssiso	$⊢ A \in V \to F {Isom}_{[\subset], {[\subset]}^{-1}} (𝒫 A, 𝒫 A)$
28		isof1o	$⊢ F {Isom}_{[\subset], {[\subset]}^{-1}} (𝒫 A, 𝒫 A) \to F : 𝒫 A \underset{1-1 onto}{⟶} 𝒫 A$
29	27 28	syl	$⊢ A \in V \to F : 𝒫 A \underset{1-1 onto}{⟶} 𝒫 A$
30		sspwuni	$⊢ F [X] \subseteq 𝒫 A \leftrightarrow ⋃ F [X] \subseteq A$
31	6 30	sylib	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to ⋃ F [X] \subseteq A$
32		elpw2g	$⊢ A \in V \to (⋃ F [X] \in 𝒫 A \leftrightarrow ⋃ F [X] \subseteq A)$
33	32	adantr	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to (⋃ F [X] \in 𝒫 A \leftrightarrow ⋃ F [X] \subseteq A)$
34	31 33	mpbird	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to ⋃ F [X] \in 𝒫 A$
35		f1ocnvfv1	$⊢ (F : 𝒫 A \underset{1-1 onto}{⟶} 𝒫 A \land ⋃ F [X] \in 𝒫 A) \to F^{-1} (F (⋃ F [X])) = ⋃ F [X]$
36	29 34 35	syl2an2r	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F^{-1} (F (⋃ F [X])) = ⋃ F [X]$
37	26 36	eqtr3id	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F (F (⋃ F [X])) = ⋃ F [X]$
38	24 37	eqtr3d	$⊢ (A \in V \land (X \subseteq 𝒫 A \land X \neq \emptyset)) \to F (⋂ X) = ⋃ F [X]$

Metamath Proof Explorer

Theorem isf34lem5

Proof