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	syl5ibr	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) → 𝐴 ∈ FinIII ) )
100	99	imp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ∈ FinIII ∨ ( 𝐴 ∖ 𝑦 ) ∈ FinIII ) ) → 𝐴 ∈ FinIII )