fin1a2s

Description: An II-infinite set can have an I-infinite part broken off and remain II-infinite. (Contributed by Stefan O'Rear, 8-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Assertion	fin1a2s	$⊢ (A \in V \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \to A \in {Fin}^{II}$

Proof

Step	Hyp	Ref	Expression
1		elpwi	$⊢ c \in 𝒫 𝒫 A \to c \subseteq 𝒫 A$
2		fin12	$⊢ x \in Fin \to x \in {Fin}^{II}$
3		fin23	$⊢ x \in {Fin}^{II} \to x \in {Fin}^{III}$
4	2 3	syl	$⊢ x \in Fin \to x \in {Fin}^{III}$
5		fin23	$⊢ A ∖ x \in {Fin}^{II} \to A ∖ x \in {Fin}^{III}$
6	4 5	orim12i	$⊢ (x \in Fin \lor A ∖ x \in {Fin}^{II}) \to (x \in {Fin}^{III} \lor A ∖ x \in {Fin}^{III})$
7	6	ralimi	$⊢ \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}) \to \forall x \in 𝒫 A (x \in {Fin}^{III} \lor A ∖ x \in {Fin}^{III})$
8		fin1a2lem8	$⊢ (A \in V \land \forall x \in 𝒫 A (x \in {Fin}^{III} \lor A ∖ x \in {Fin}^{III})) \to A \in {Fin}^{III}$
9	7 8	sylan2	$⊢ (A \in V \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \to A \in {Fin}^{III}$
10	9	adantr	$⊢ ((A \in V \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \to A \in {Fin}^{III}$
11		simplrl	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land (\neg ⋃ c \in c \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}))) \to c \subseteq 𝒫 A$
12		simprrr	$⊢ (A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \to [\subset] Or c$
13	12	adantr	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land (\neg ⋃ c \in c \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}))) \to [\subset] Or c$
14		simprl	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land (\neg ⋃ c \in c \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}))) \to \neg ⋃ c \in c$
15		simplrl	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \to c \subseteq 𝒫 A$
16		ssralv	$⊢ c \subseteq 𝒫 A \to (\forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}) \to \forall x \in c (x \in Fin \lor A ∖ x \in {Fin}^{II}))$
17	15 16	syl	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \to (\forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}) \to \forall x \in c (x \in Fin \lor A ∖ x \in {Fin}^{II}))$
18		idd	$⊢ (((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \land x \in c) \to (x \in Fin \to x \in Fin)$
19		fin1a2lem13	$⊢ ((c \subseteq 𝒫 A \land [\subset] Or c \land \neg ⋃ c \in c) \land (\neg x \in Fin \land x \in c)) \to \neg A ∖ x \in {Fin}^{II}$
20	19	ex	$⊢ (c \subseteq 𝒫 A \land [\subset] Or c \land \neg ⋃ c \in c) \to ((\neg x \in Fin \land x \in c) \to \neg A ∖ x \in {Fin}^{II})$
21	20	3expa	$⊢ ((c \subseteq 𝒫 A \land [\subset] Or c) \land \neg ⋃ c \in c) \to ((\neg x \in Fin \land x \in c) \to \neg A ∖ x \in {Fin}^{II})$
22	21	adantlrl	$⊢ ((c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c)) \land \neg ⋃ c \in c) \to ((\neg x \in Fin \land x \in c) \to \neg A ∖ x \in {Fin}^{II})$
23	22	adantll	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \to ((\neg x \in Fin \land x \in c) \to \neg A ∖ x \in {Fin}^{II})$
24	23	imp	$⊢ (((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \land (\neg x \in Fin \land x \in c)) \to \neg A ∖ x \in {Fin}^{II}$
25	24	ancom2s	$⊢ (((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \land (x \in c \land \neg x \in Fin)) \to \neg A ∖ x \in {Fin}^{II}$
26	25	expr	$⊢ (((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \land x \in c) \to (\neg x \in Fin \to \neg A ∖ x \in {Fin}^{II})$
27	26	con4d	$⊢ (((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \land x \in c) \to (A ∖ x \in {Fin}^{II} \to x \in Fin)$
28	18 27	jaod	$⊢ (((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \land x \in c) \to ((x \in Fin \lor A ∖ x \in {Fin}^{II}) \to x \in Fin)$
29	28	ralimdva	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \to (\forall x \in c (x \in Fin \lor A ∖ x \in {Fin}^{II}) \to \forall x \in c x \in Fin)$
30	17 29	syld	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \to (\forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}) \to \forall x \in c x \in Fin)$
31	30	impr	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land (\neg ⋃ c \in c \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}))) \to \forall x \in c x \in Fin$
32		dfss3	$⊢ c \subseteq Fin \leftrightarrow \forall x \in c x \in Fin$
33	31 32	sylibr	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land (\neg ⋃ c \in c \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}))) \to c \subseteq Fin$
34		simprrl	$⊢ (A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \to c \neq \emptyset$
35	34	adantr	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land (\neg ⋃ c \in c \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}))) \to c \neq \emptyset$
36		fin1a2lem12	$⊢ ((c \subseteq 𝒫 A \land [\subset] Or c \land \neg ⋃ c \in c) \land (c \subseteq Fin \land c \neq \emptyset)) \to \neg A \in {Fin}^{III}$
37	11 13 14 33 35 36	syl32anc	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land (\neg ⋃ c \in c \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}))) \to \neg A \in {Fin}^{III}$
38	37	expr	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \neg ⋃ c \in c) \to (\forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II}) \to \neg A \in {Fin}^{III})$
39	38	impancom	$⊢ ((A \in V \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \to (\neg ⋃ c \in c \to \neg A \in {Fin}^{III})$
40	39	an32s	$⊢ ((A \in V \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \to (\neg ⋃ c \in c \to \neg A \in {Fin}^{III})$
41	10 40	mt4d	$⊢ ((A \in V \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \land (c \subseteq 𝒫 A \land (c \neq \emptyset \land [\subset] Or c))) \to ⋃ c \in c$
42	41	exp32	$⊢ (A \in V \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \to (c \subseteq 𝒫 A \to ((c \neq \emptyset \land [\subset] Or c) \to ⋃ c \in c))$
43	1 42	syl5	$⊢ (A \in V \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \to (c \in 𝒫 𝒫 A \to ((c \neq \emptyset \land [\subset] Or c) \to ⋃ c \in c))$
44	43	ralrimiv	$⊢ (A \in V \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \to \forall c \in 𝒫 𝒫 A ((c \neq \emptyset \land [\subset] Or c) \to ⋃ c \in c)$
45		isfin2	$⊢ A \in V \to (A \in {Fin}^{II} \leftrightarrow \forall c \in 𝒫 𝒫 A ((c \neq \emptyset \land [\subset] Or c) \to ⋃ c \in c))$
46	45	adantr	$⊢ (A \in V \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \to (A \in {Fin}^{II} \leftrightarrow \forall c \in 𝒫 𝒫 A ((c \neq \emptyset \land [\subset] Or c) \to ⋃ c \in c))$
47	44 46	mpbird	$⊢ (A \in V \land \forall x \in 𝒫 A (x \in Fin \lor A ∖ x \in {Fin}^{II})) \to A \in {Fin}^{II}$

Metamath Proof Explorer

Theorem fin1a2s

Proof