Metamath Proof Explorer

Theorem fin2i

Description: Property of a II-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

		Ref	Expression
	Assertion	fin2i	$⊢ ((A \in {Fin}^{II} \land B \subseteq 𝒫 A) \land (B \neq \emptyset \land [\subset] Or B)) \to ⋃ B \in B$

Proof

Step	Hyp	Ref	Expression
1		neeq1	$⊢ y = B \to (y \neq \emptyset \leftrightarrow B \neq \emptyset)$
2		soeq2	$⊢ y = B \to ([\subset] Or y \leftrightarrow [\subset] Or B)$
3	1 2	anbi12d	$⊢ y = B \to ((y \neq \emptyset \land [\subset] Or y) \leftrightarrow (B \neq \emptyset \land [\subset] Or B))$
4		unieq	$⊢ y = B \to ⋃ y = ⋃ B$
5		id	$⊢ y = B \to y = B$
6	4 5	eleq12d	$⊢ y = B \to (⋃ y \in y \leftrightarrow ⋃ B \in B)$
7	3 6	imbi12d	$⊢ y = B \to (((y \neq \emptyset \land [\subset] Or y) \to ⋃ y \in y) \leftrightarrow ((B \neq \emptyset \land [\subset] Or B) \to ⋃ B \in B))$
8		isfin2	$⊢ A \in {Fin}^{II} \to (A \in {Fin}^{II} \leftrightarrow \forall y \in 𝒫 𝒫 A ((y \neq \emptyset \land [\subset] Or y) \to ⋃ y \in y))$
9	8	ibi	$⊢ A \in {Fin}^{II} \to \forall y \in 𝒫 𝒫 A ((y \neq \emptyset \land [\subset] Or y) \to ⋃ y \in y)$
10	9	adantr	$⊢ (A \in {Fin}^{II} \land B \subseteq 𝒫 A) \to \forall y \in 𝒫 𝒫 A ((y \neq \emptyset \land [\subset] Or y) \to ⋃ y \in y)$
11		pwexg	$⊢ A \in {Fin}^{II} \to 𝒫 A \in V$
12		elpw2g	$⊢ 𝒫 A \in V \to (B \in 𝒫 𝒫 A \leftrightarrow B \subseteq 𝒫 A)$
13	11 12	syl	$⊢ A \in {Fin}^{II} \to (B \in 𝒫 𝒫 A \leftrightarrow B \subseteq 𝒫 A)$
14	13	biimpar	$⊢ (A \in {Fin}^{II} \land B \subseteq 𝒫 A) \to B \in 𝒫 𝒫 A$
15	7 10 14	rspcdva	$⊢ (A \in {Fin}^{II} \land B \subseteq 𝒫 A) \to ((B \neq \emptyset \land [\subset] Or B) \to ⋃ B \in B)$
16	15	imp	$⊢ ((A \in {Fin}^{II} \land B \subseteq 𝒫 A) \land (B \neq \emptyset \land [\subset] Or B)) \to ⋃ B \in B$