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

Metamath Proof Explorer

Theorem fin1a2lem7

Description: Lemma for fin1a2 . Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014)

Ref Expression
Hypotheses fin1a2lem.b ⊢ 𝐸 = ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) )
fin1a2lem.aa ⊢ 𝑆 = ( 𝑥 ∈ On ↦ suc 𝑥 )
Assertion fin1a2lem7 ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) ) → 𝐴 ∈ FinIII )

Proof

Step Hyp Ref Expression
1 fin1a2lem.b ⊢ 𝐸 = ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) )
2 fin1a2lem.aa ⊢ 𝑆 = ( 𝑥 ∈ On ↦ suc 𝑥 )
3 peano1 ⊢ ∅ ∈ ω
4 ne0i ⊢ ( ∅ ∈ ω → ω ≠ ∅ )
5 brwdomn0 ⊢ ( ω ≠ ∅ → ( ω ≼* 𝐴 ↔ ∃ 𝑓 𝑓 : 𝐴 –onto→ ω ) )
6 3 4 5 mp2b ⊢ ( ω ≼* 𝐴 ↔ ∃ 𝑓 𝑓 : 𝐴 –onto→ ω )
7 vex ⊢ 𝑓 ∈ V
8 fof ⊢ ( 𝑓 : 𝐴 –onto→ ω → 𝑓 : 𝐴 ⟶ ω )
9 dmfex ⊢ ( ( 𝑓 ∈ V ∧ 𝑓 : 𝐴 ⟶ ω ) → 𝐴 ∈ V )
10 7 8 9 sylancr ⊢ ( 𝑓 : 𝐴 –onto→ ω → 𝐴 ∈ V )
11 cnvimass ⊢ ( ◡ 𝑓 “ ran 𝐸 ) ⊆ dom 𝑓
12 11 8 fssdm ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ◡ 𝑓 “ ran 𝐸 ) ⊆ 𝐴 )
13 10 12 sselpwd ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ◡ 𝑓 “ ran 𝐸 ) ∈ 𝒫 𝐴 )
14 1 fin1a2lem4 ⊢ 𝐸 : ω –1-1→ ω
15 f1cnv ⊢ ( 𝐸 : ω –1-1→ ω → ◡ 𝐸 : ran 𝐸 –1-1-onto→ ω )
16 f1ofo ⊢ ( ◡ 𝐸 : ran 𝐸 –1-1-onto→ ω → ◡ 𝐸 : ran 𝐸 –onto→ ω )
17 14 15 16 mp2b ⊢ ◡ 𝐸 : ran 𝐸 –onto→ ω
18 fofun ⊢ ( ◡ 𝐸 : ran 𝐸 –onto→ ω → Fun ◡ 𝐸 )
19 17 18 ax-mp ⊢ Fun ◡ 𝐸
20 7 resex ⊢ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ V
21 cofunexg ⊢ ( ( Fun ◡ 𝐸 ∧ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ V ) → ( ◡ 𝐸 ∘ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ∈ V )
22 19 20 21 mp2an ⊢ ( ◡ 𝐸 ∘ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ∈ V
23 fofun ⊢ ( 𝑓 : 𝐴 –onto→ ω → Fun 𝑓 )
24 fores ⊢ ( ( Fun 𝑓 ∧ ( ◡ 𝑓 “ ran 𝐸 ) ⊆ dom 𝑓 ) → ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ( 𝑓 “ ( ◡ 𝑓 “ ran 𝐸 ) ) )
25 23 11 24 sylancl ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ( 𝑓 “ ( ◡ 𝑓 “ ran 𝐸 ) ) )
26 f1f ⊢ ( 𝐸 : ω –1-1→ ω → 𝐸 : ω ⟶ ω )
27 frn ⊢ ( 𝐸 : ω ⟶ ω → ran 𝐸 ⊆ ω )
28 14 26 27 mp2b ⊢ ran 𝐸 ⊆ ω
29 foimacnv ⊢ ( ( 𝑓 : 𝐴 –onto→ ω ∧ ran 𝐸 ⊆ ω ) → ( 𝑓 “ ( ◡ 𝑓 “ ran 𝐸 ) ) = ran 𝐸 )
30 28 29 mpan2 ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( 𝑓 “ ( ◡ 𝑓 “ ran 𝐸 ) ) = ran 𝐸 )
31 foeq3 ⊢ ( ( 𝑓 “ ( ◡ 𝑓 “ ran 𝐸 ) ) = ran 𝐸 → ( ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ( 𝑓 “ ( ◡ 𝑓 “ ran 𝐸 ) ) ↔ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ran 𝐸 ) )
32 30 31 syl ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ( 𝑓 “ ( ◡ 𝑓 “ ran 𝐸 ) ) ↔ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ran 𝐸 ) )
33 25 32 mpbid ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ran 𝐸 )
34 foco ⊢ ( ( ◡ 𝐸 : ran 𝐸 –onto→ ω ∧ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ran 𝐸 ) → ( ◡ 𝐸 ∘ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ω )
35 17 33 34 sylancr ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ◡ 𝐸 ∘ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ω )
36 fowdom ⊢ ( ( ( ◡ 𝐸 ∘ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ∈ V ∧ ( ◡ 𝐸 ∘ ( 𝑓 ↾ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( ◡ 𝑓 “ ran 𝐸 ) –onto→ ω ) → ω ≼* ( ◡ 𝑓 “ ran 𝐸 ) )
37 22 35 36 sylancr ⊢ ( 𝑓 : 𝐴 –onto→ ω → ω ≼* ( ◡ 𝑓 “ ran 𝐸 ) )
38 7 cnvex ⊢ ◡ 𝑓 ∈ V
39 38 imaex ⊢ ( ◡ 𝑓 “ ran 𝐸 ) ∈ V
40 isfin3-2 ⊢ ( ( ◡ 𝑓 “ ran 𝐸 ) ∈ V → ( ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII ↔ ¬ ω ≼* ( ◡ 𝑓 “ ran 𝐸 ) ) )
41 39 40 ax-mp ⊢ ( ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII ↔ ¬ ω ≼* ( ◡ 𝑓 “ ran 𝐸 ) )
42 41 con2bii ⊢ ( ω ≼* ( ◡ 𝑓 “ ran 𝐸 ) ↔ ¬ ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII )
43 37 42 sylib ⊢ ( 𝑓 : 𝐴 –onto→ ω → ¬ ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII )
44 1 2 fin1a2lem6 ⊢ ( 𝑆 ↾ ran 𝐸 ) : ran 𝐸 –1-1-onto→ ( ω ∖ ran 𝐸 )
45 f1ocnv ⊢ ( ( 𝑆 ↾ ran 𝐸 ) : ran 𝐸 –1-1-onto→ ( ω ∖ ran 𝐸 ) → ◡ ( 𝑆 ↾ ran 𝐸 ) : ( ω ∖ ran 𝐸 ) –1-1-onto→ ran 𝐸 )
46 f1ofo ⊢ ( ◡ ( 𝑆 ↾ ran 𝐸 ) : ( ω ∖ ran 𝐸 ) –1-1-onto→ ran 𝐸 → ◡ ( 𝑆 ↾ ran 𝐸 ) : ( ω ∖ ran 𝐸 ) –onto→ ran 𝐸 )
47 44 45 46 mp2b ⊢ ◡ ( 𝑆 ↾ ran 𝐸 ) : ( ω ∖ ran 𝐸 ) –onto→ ran 𝐸
48 foco ⊢ ( ( ◡ 𝐸 : ran 𝐸 –onto→ ω ∧ ◡ ( 𝑆 ↾ ran 𝐸 ) : ( ω ∖ ran 𝐸 ) –onto→ ran 𝐸 ) → ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) : ( ω ∖ ran 𝐸 ) –onto→ ω )
49 17 47 48 mp2an ⊢ ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) : ( ω ∖ ran 𝐸 ) –onto→ ω
50 fofun ⊢ ( ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) : ( ω ∖ ran 𝐸 ) –onto→ ω → Fun ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) )
51 49 50 ax-mp ⊢ Fun ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) )
52 7 resex ⊢ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ∈ V
53 cofunexg ⊢ ( ( Fun ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) ∧ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ∈ V ) → ( ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) ∘ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ) ∈ V )
54 51 52 53 mp2an ⊢ ( ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) ∘ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ) ∈ V
55 difss ⊢ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ⊆ 𝐴
56 8 fdmd ⊢ ( 𝑓 : 𝐴 –onto→ ω → dom 𝑓 = 𝐴 )
57 55 56 sseqtrrid ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ⊆ dom 𝑓 )
58 fores ⊢ ( ( Fun 𝑓 ∧ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ⊆ dom 𝑓 ) → ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ( 𝑓 “ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) )
59 23 57 58 syl2anc ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ( 𝑓 “ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) )
60 funcnvcnv ⊢ ( Fun 𝑓 → Fun ◡ ◡ 𝑓 )
61 imadif ⊢ ( Fun ◡ ◡ 𝑓 → ( ◡ 𝑓 “ ( ω ∖ ran 𝐸 ) ) = ( ( ◡ 𝑓 “ ω ) ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) )
62 23 60 61 3syl ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ◡ 𝑓 “ ( ω ∖ ran 𝐸 ) ) = ( ( ◡ 𝑓 “ ω ) ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) )
63 62 imaeq2d ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( 𝑓 “ ( ◡ 𝑓 “ ( ω ∖ ran 𝐸 ) ) ) = ( 𝑓 “ ( ( ◡ 𝑓 “ ω ) ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) )
64 difss ⊢ ( ω ∖ ran 𝐸 ) ⊆ ω
65 foimacnv ⊢ ( ( 𝑓 : 𝐴 –onto→ ω ∧ ( ω ∖ ran 𝐸 ) ⊆ ω ) → ( 𝑓 “ ( ◡ 𝑓 “ ( ω ∖ ran 𝐸 ) ) ) = ( ω ∖ ran 𝐸 ) )
66 64 65 mpan2 ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( 𝑓 “ ( ◡ 𝑓 “ ( ω ∖ ran 𝐸 ) ) ) = ( ω ∖ ran 𝐸 ) )
67 fimacnv ⊢ ( 𝑓 : 𝐴 ⟶ ω → ( ◡ 𝑓 “ ω ) = 𝐴 )
68 8 67 syl ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ◡ 𝑓 “ ω ) = 𝐴 )
69 68 difeq1d ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ( ◡ 𝑓 “ ω ) ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) = ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) )
70 69 imaeq2d ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( 𝑓 “ ( ( ◡ 𝑓 “ ω ) ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) = ( 𝑓 “ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) )
71 63 66 70 3eqtr3rd ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( 𝑓 “ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) = ( ω ∖ ran 𝐸 ) )
72 foeq3 ⊢ ( ( 𝑓 “ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) = ( ω ∖ ran 𝐸 ) → ( ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ( 𝑓 “ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ↔ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ( ω ∖ ran 𝐸 ) ) )
73 71 72 syl ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ( 𝑓 “ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ↔ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ( ω ∖ ran 𝐸 ) ) )
74 59 73 mpbid ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ( ω ∖ ran 𝐸 ) )
75 foco ⊢ ( ( ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) : ( ω ∖ ran 𝐸 ) –onto→ ω ∧ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ( ω ∖ ran 𝐸 ) ) → ( ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) ∘ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ω )
76 49 74 75 sylancr ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) ∘ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ω )
77 fowdom ⊢ ( ( ( ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) ∘ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ) ∈ V ∧ ( ( ◡ 𝐸 ∘ ◡ ( 𝑆 ↾ ran 𝐸 ) ) ∘ ( 𝑓 ↾ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) ) : ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) –onto→ ω ) → ω ≼* ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) )
78 54 76 77 sylancr ⊢ ( 𝑓 : 𝐴 –onto→ ω → ω ≼* ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) )
79 difexg ⊢ ( 𝐴 ∈ V → ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ V )
80 isfin3-2 ⊢ ( ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ V → ( ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII ↔ ¬ ω ≼* ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) )
81 10 79 80 3syl ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII ↔ ¬ ω ≼* ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ) )
82 81 con2bid ⊢ ( 𝑓 : 𝐴 –onto→ ω → ( ω ≼* ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ↔ ¬ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII ) )
83 78 82 mpbid ⊢ ( 𝑓 : 𝐴 –onto→ ω → ¬ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII )
84 eleq1 ⊢ ( 𝑦 = ( ◡ 𝑓 “ ran 𝐸 ) → ( 𝑦 ∈ FinIII ↔ ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII ) )
85 difeq2 ⊢ ( 𝑦 = ( ◡ 𝑓 “ ran 𝐸 ) → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) )
86 85 eleq1d ⊢ ( 𝑦 = ( ◡ 𝑓 “ ran 𝐸 ) → ( ( 𝐴 ∖ 𝑦 ) ∈ FinIII ↔ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII ) )
87 84 86 orbi12d ⊢ ( 𝑦 = ( ◡ 𝑓 “ ran 𝐸 ) → ( ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) ↔ ( ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII ∨ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII ) ) )
88 87 notbid ⊢ ( 𝑦 = ( ◡ 𝑓 “ ran 𝐸 ) → ( ¬ ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) ↔ ¬ ( ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII ∨ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII ) ) )
89 ioran ⊢ ( ¬ ( ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII ∨ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII ) ↔ ( ¬ ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII ∧ ¬ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII ) )
90 88 89 bitrdi ⊢ ( 𝑦 = ( ◡ 𝑓 “ ran 𝐸 ) → ( ¬ ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) ↔ ( ¬ ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII ∧ ¬ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII ) ) )
91 90 rspcev ⊢ ( ( ( ◡ 𝑓 “ ran 𝐸 ) ∈ 𝒫 𝐴 ∧ ( ¬ ( ◡ 𝑓 “ ran 𝐸 ) ∈ FinIII ∧ ¬ ( 𝐴 ∖ ( ◡ 𝑓 “ ran 𝐸 ) ) ∈ FinIII ) ) → ∃ 𝑦 ∈ 𝒫 𝐴 ¬ ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) )
92 13 43 83 91 syl12anc ⊢ ( 𝑓 : 𝐴 –onto→ ω → ∃ 𝑦 ∈ 𝒫 𝐴 ¬ ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) )
93 rexnal ⊢ ( ∃ 𝑦 ∈ 𝒫 𝐴 ¬ ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) ↔ ¬ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) )
94 92 93 sylib ⊢ ( 𝑓 : 𝐴 –onto→ ω → ¬ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) )
95 94 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –onto→ ω → ¬ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) )
96 6 95 sylbi ⊢ ( ω ≼* 𝐴 → ¬ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) )
97 96 con2i ⊢ ( ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) → ¬ ω ≼* 𝐴 )
98 isfin3-2 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIII ↔ ¬ ω ≼* 𝐴 ) )
99 97 98 imbitrrid ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) → 𝐴 ∈ FinIII ) )
100 99 imp ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) ) → 𝐴 ∈ FinIII )