Theorem 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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) → 𝐴 ∈ FinII )

Proof

Step	Hyp	Ref	Expression
1		elpwi	⊢ ( 𝑐 ∈ 𝒫 𝒫 𝐴 → 𝑐 ⊆ 𝒫 𝐴 )
2		fin12	⊢ ( 𝑥 ∈ Fin → 𝑥 ∈ FinII )
3		fin23	⊢ ( 𝑥 ∈ FinII → 𝑥 ∈ FinIII )
4	2 3	syl	⊢ ( 𝑥 ∈ Fin → 𝑥 ∈ FinIII )
5		fin23	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ FinII → ( 𝐴 ∖ 𝑥 ) ∈ FinIII )
6	4 5	orim12i	⊢ ( ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) → ( 𝑥 ∈ FinIII ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinIII ) )
7	6	ralimi	⊢ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) → ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ FinIII ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinIII ) )
8		fin1a2lem8	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ FinIII ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinIII ) ) → 𝐴 ∈ FinIII )
9	7 8	sylan2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) → 𝐴 ∈ FinIII )
10	9	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) → 𝐴 ∈ FinIII )
11		simplrl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ( ¬ ∪ 𝑐 ∈ 𝑐 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) ) → 𝑐 ⊆ 𝒫 𝐴 )
12		simprrr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) → [⊊] Or 𝑐 )
13	12	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ( ¬ ∪ 𝑐 ∈ 𝑐 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) ) → [⊊] Or 𝑐 )
14		simprl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ( ¬ ∪ 𝑐 ∈ 𝑐 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) ) → ¬ ∪ 𝑐 ∈ 𝑐 )
15		simplrl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) → 𝑐 ⊆ 𝒫 𝐴 )
16		ssralv	⊢ ( 𝑐 ⊆ 𝒫 𝐴 → ( ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) → ∀ 𝑥 ∈ 𝑐 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) )
17	15 16	syl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) → ( ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) → ∀ 𝑥 ∈ 𝑐 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) )
18		idd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) ∧ 𝑥 ∈ 𝑐 ) → ( 𝑥 ∈ Fin → 𝑥 ∈ Fin ) )
19		fin1a2lem13	⊢ ( ( ( 𝑐 ⊆ 𝒫 𝐴 ∧ [⊊] Or 𝑐 ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) ∧ ( ¬ 𝑥 ∈ Fin ∧ 𝑥 ∈ 𝑐 ) ) → ¬ ( 𝐴 ∖ 𝑥 ) ∈ FinII )
20	19	ex	⊢ ( ( 𝑐 ⊆ 𝒫 𝐴 ∧ [⊊] Or 𝑐 ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) → ( ( ¬ 𝑥 ∈ Fin ∧ 𝑥 ∈ 𝑐 ) → ¬ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) )
21	20	3expa	⊢ ( ( ( 𝑐 ⊆ 𝒫 𝐴 ∧ [⊊] Or 𝑐 ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) → ( ( ¬ 𝑥 ∈ Fin ∧ 𝑥 ∈ 𝑐 ) → ¬ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) )
22	21	adantlrl	⊢ ( ( ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) → ( ( ¬ 𝑥 ∈ Fin ∧ 𝑥 ∈ 𝑐 ) → ¬ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) )
23	22	adantll	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) → ( ( ¬ 𝑥 ∈ Fin ∧ 𝑥 ∈ 𝑐 ) → ¬ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) )
24	23	imp	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) ∧ ( ¬ 𝑥 ∈ Fin ∧ 𝑥 ∈ 𝑐 ) ) → ¬ ( 𝐴 ∖ 𝑥 ) ∈ FinII )
25	24	ancom2s	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) ∧ ( 𝑥 ∈ 𝑐 ∧ ¬ 𝑥 ∈ Fin ) ) → ¬ ( 𝐴 ∖ 𝑥 ) ∈ FinII )
26	25	expr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) ∧ 𝑥 ∈ 𝑐 ) → ( ¬ 𝑥 ∈ Fin → ¬ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) )
27	26	con4d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) ∧ 𝑥 ∈ 𝑐 ) → ( ( 𝐴 ∖ 𝑥 ) ∈ FinII → 𝑥 ∈ Fin ) )
28	18 27	jaod	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) ∧ 𝑥 ∈ 𝑐 ) → ( ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) → 𝑥 ∈ Fin ) )
29	28	ralimdva	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) → ( ∀ 𝑥 ∈ 𝑐 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) → ∀ 𝑥 ∈ 𝑐 𝑥 ∈ Fin ) )
30	17 29	syld	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) → ( ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) → ∀ 𝑥 ∈ 𝑐 𝑥 ∈ Fin ) )
31	30	impr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ( ¬ ∪ 𝑐 ∈ 𝑐 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) ) → ∀ 𝑥 ∈ 𝑐 𝑥 ∈ Fin )
32		dfss3	⊢ ( 𝑐 ⊆ Fin ↔ ∀ 𝑥 ∈ 𝑐 𝑥 ∈ Fin )
33	31 32	sylibr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ( ¬ ∪ 𝑐 ∈ 𝑐 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) ) → 𝑐 ⊆ Fin )
34		simprrl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) → 𝑐 ≠ ∅ )
35	34	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ( ¬ ∪ 𝑐 ∈ 𝑐 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) ) → 𝑐 ≠ ∅ )
36		fin1a2lem12	⊢ ( ( ( 𝑐 ⊆ 𝒫 𝐴 ∧ [⊊] Or 𝑐 ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) ∧ ( 𝑐 ⊆ Fin ∧ 𝑐 ≠ ∅ ) ) → ¬ 𝐴 ∈ FinIII )
37	11 13 14 33 35 36	syl32anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ( ¬ ∪ 𝑐 ∈ 𝑐 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) ) → ¬ 𝐴 ∈ FinIII )
38	37	expr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ¬ ∪ 𝑐 ∈ 𝑐 ) → ( ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) → ¬ 𝐴 ∈ FinIII ) )
39	38	impancom	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) → ( ¬ ∪ 𝑐 ∈ 𝑐 → ¬ 𝐴 ∈ FinIII ) )
40	39	an32s	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) → ( ¬ ∪ 𝑐 ∈ 𝑐 → ¬ 𝐴 ∈ FinIII ) )
41	10 40	mt4d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) ∧ ( 𝑐 ⊆ 𝒫 𝐴 ∧ ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) ) ) → ∪ 𝑐 ∈ 𝑐 )
42	41	exp32	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) → ( 𝑐 ⊆ 𝒫 𝐴 → ( ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) → ∪ 𝑐 ∈ 𝑐 ) ) )
43	1 42	syl5	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) → ( 𝑐 ∈ 𝒫 𝒫 𝐴 → ( ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) → ∪ 𝑐 ∈ 𝑐 ) ) )
44	43	ralrimiv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) → ∀ 𝑐 ∈ 𝒫 𝒫 𝐴 ( ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) → ∪ 𝑐 ∈ 𝑐 ) )
45		isfin2	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinII ↔ ∀ 𝑐 ∈ 𝒫 𝒫 𝐴 ( ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) → ∪ 𝑐 ∈ 𝑐 ) ) )
46	45	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) → ( 𝐴 ∈ FinII ↔ ∀ 𝑐 ∈ 𝒫 𝒫 𝐴 ( ( 𝑐 ≠ ∅ ∧ [⊊] Or 𝑐 ) → ∪ 𝑐 ∈ 𝑐 ) ) )
47	44 46	mpbird	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑥 ∈ Fin ∨ ( 𝐴 ∖ 𝑥 ) ∈ FinII ) ) → 𝐴 ∈ FinII )