This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )