fin1a2lem7 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fin1a2lem7		Structured version Visualization version GIF version

Theorem fin1a2lem7 10521

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

**Hypotheses**
Ref	Expression
fin1a2lem.b	⊢ 𝐸 = (𝑥 ∈ ω ↦ (2_o ·_o 𝑥))
fin1a2lem.aa	⊢ 𝑆 = (𝑥 ∈ On ↦ suc 𝑥)

**Assertion**
Ref	Expression
fin1a2lem7	⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III)) → 𝐴 ∈ Fin^III)

Distinct variable groups: 𝑦,𝐴 𝑦,𝐸 Allowed substitution hints: 𝐴(𝑥) 𝑆(𝑥, 𝑦) 𝐸(𝑥) 𝑉(𝑥, 𝑦)

Proof of Theorem fin1a2lem7 Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano1 7932	. . . . . 6 ⊢ ∅ ∈ ω
2		ne0i 4290	. . . . . 6 ⊢ (∅ ∈ ω → ω ≠ ∅)
3		brwdomn0 9598	. . . . . 6 ⊢ (ω ≠ ∅ → (ω ≼^* 𝐴 ↔ ∃𝑓 𝑓:𝐴⟶ontoω))
4	1, 2, 3	mp2b 10	. . . . 5 ⊢ (ω ≼^* 𝐴 ↔ ∃𝑓 𝑓:𝐴⟶ontoω)
5		vex 3458	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
6		fof 6824	. . . . . . . . . 10 ⊢ (𝑓:𝐴⟶ontoω → 𝑓:𝐴⟶ω)
7		dmfex 7949	. . . . . . . . . 10 ⊢ ((𝑓 ∈ V ∧ 𝑓:𝐴⟶ω) → 𝐴 ∈ V)
8	5, 6, 7	sylancr 599	. . . . . . . . 9 ⊢ (𝑓:𝐴⟶ontoω → 𝐴 ∈ V)
9		cnvimass 6215	. . . . . . . . . 10 ⊢ (^◡𝑓 “ ran 𝐸) ⊆ dom 𝑓
10	9, 6	fssdm 6757	. . . . . . . . 9 ⊢ (𝑓:𝐴⟶ontoω → (^◡𝑓 “ ran 𝐸) ⊆ 𝐴)
11	8, 10	sselpwd 5295	. . . . . . . 8 ⊢ (𝑓:𝐴⟶ontoω → (^◡𝑓 “ ran 𝐸) ∈ 𝒫 𝐴)
12		fin1a2lem.b	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝑥 ∈ ω ↦ (2_o ·_o 𝑥))
13	12	fin1a2lem4 10518	. . . . . . . . . . . . 13 ⊢ 𝐸:ω⟶1-1ω
14		f1cnv 6877	. . . . . . . . . . . . 13 ⊢ (𝐸:ω⟶1-1ω → ^◡𝐸:ran 𝐸⟶1-1ontoω)
15		f1ofo 6860	. . . . . . . . . . . . 13 ⊢ (^◡𝐸:ran 𝐸⟶1-1ontoω → ^◡𝐸:ran 𝐸⟶ontoω)
16	13, 14, 15	mp2b 10	. . . . . . . . . . . 12 ⊢ ^◡𝐸:ran 𝐸⟶ontoω
17		fofun 6825	. . . . . . . . . . . 12 ⊢ (^◡𝐸:ran 𝐸⟶ontoω → Fun ^◡𝐸)
18	16, 17	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun ^◡𝐸
19	5	resex 6034	. . . . . . . . . . 11 ⊢ (𝑓 ↾ (^◡𝑓 “ ran 𝐸)) ∈ V
20		cofunexg 7993	. . . . . . . . . . 11 ⊢ ((Fun ^◡𝐸 ∧ (𝑓 ↾ (^◡𝑓 “ ran 𝐸)) ∈ V) → (^◡𝐸 ∘ (𝑓 ↾ (^◡𝑓 “ ran 𝐸))) ∈ V)
21	18, 19, 20	mp2an 705	. . . . . . . . . 10 ⊢ (^◡𝐸 ∘ (𝑓 ↾ (^◡𝑓 “ ran 𝐸))) ∈ V
22		fofun 6825	. . . . . . . . . . . . 13 ⊢ (𝑓:𝐴⟶ontoω → Fun 𝑓)
23		fores 6834	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑓 ∧ (^◡𝑓 “ ran 𝐸) ⊆ dom 𝑓) → (𝑓 ↾ (^◡𝑓 “ ran 𝐸)):(^◡𝑓 “ ran 𝐸)⟶onto(𝑓 “ (^◡𝑓 “ ran 𝐸)))
24	22, 9, 23	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝑓:𝐴⟶ontoω → (𝑓 ↾ (^◡𝑓 “ ran 𝐸)):(^◡𝑓 “ ran 𝐸)⟶onto(𝑓 “ (^◡𝑓 “ ran 𝐸)))
25		f1f 6806	. . . . . . . . . . . . . . 15 ⊢ (𝐸:ω⟶1-1ω → 𝐸:ω⟶ω)
26		frn 6745	. . . . . . . . . . . . . . 15 ⊢ (𝐸:ω⟶ω → ran 𝐸 ⊆ ω)
27	13, 25, 26	mp2b 10	. . . . . . . . . . . . . 14 ⊢ ran 𝐸 ⊆ ω
28		foimacnv 6870	. . . . . . . . . . . . . 14 ⊢ ((𝑓:𝐴⟶ontoω ∧ ran 𝐸 ⊆ ω) → (𝑓 “ (^◡𝑓 “ ran 𝐸)) = ran 𝐸)
29	27, 28	mpan2 704	. . . . . . . . . . . . 13 ⊢ (𝑓:𝐴⟶ontoω → (𝑓 “ (^◡𝑓 “ ran 𝐸)) = ran 𝐸)
30		foeq3 6822	. . . . . . . . . . . . 13 ⊢ ((𝑓 “ (^◡𝑓 “ ran 𝐸)) = ran 𝐸 → ((𝑓 ↾ (^◡𝑓 “ ran 𝐸)):(^◡𝑓 “ ran 𝐸)⟶onto(𝑓 “ (^◡𝑓 “ ran 𝐸)) ↔ (𝑓 ↾ (^◡𝑓 “ ran 𝐸)):(^◡𝑓 “ ran 𝐸)⟶ontoran 𝐸))
31	29, 30	syl 18	. . . . . . . . . . . 12 ⊢ (𝑓:𝐴⟶ontoω → ((𝑓 ↾ (^◡𝑓 “ ran 𝐸)):(^◡𝑓 “ ran 𝐸)⟶onto(𝑓 “ (^◡𝑓 “ ran 𝐸)) ↔ (𝑓 ↾ (^◡𝑓 “ ran 𝐸)):(^◡𝑓 “ ran 𝐸)⟶ontoran 𝐸))
32	24, 31	mpbid 235	. . . . . . . . . . 11 ⊢ (𝑓:𝐴⟶ontoω → (𝑓 ↾ (^◡𝑓 “ ran 𝐸)):(^◡𝑓 “ ran 𝐸)⟶ontoran 𝐸)
33		foco 6838	. . . . . . . . . . 11 ⊢ ((^◡𝐸:ran 𝐸⟶ontoω ∧ (𝑓 ↾ (^◡𝑓 “ ran 𝐸)):(^◡𝑓 “ ran 𝐸)⟶ontoran 𝐸) → (^◡𝐸 ∘ (𝑓 ↾ (^◡𝑓 “ ran 𝐸))):(^◡𝑓 “ ran 𝐸)⟶ontoω)
34	16, 32, 33	sylancr 599	. . . . . . . . . 10 ⊢ (𝑓:𝐴⟶ontoω → (^◡𝐸 ∘ (𝑓 ↾ (^◡𝑓 “ ran 𝐸))):(^◡𝑓 “ ran 𝐸)⟶ontoω)
35		fowdom 9600	. . . . . . . . . 10 ⊢ (((^◡𝐸 ∘ (𝑓 ↾ (^◡𝑓 “ ran 𝐸))) ∈ V ∧ (^◡𝐸 ∘ (𝑓 ↾ (^◡𝑓 “ ran 𝐸))):(^◡𝑓 “ ran 𝐸)⟶ontoω) → ω ≼^* (^◡𝑓 “ ran 𝐸))
36	21, 34, 35	sylancr 599	. . . . . . . . 9 ⊢ (𝑓:𝐴⟶ontoω → ω ≼^* (^◡𝑓 “ ran 𝐸))
37	5	cnvex 7969	. . . . . . . . . . . 12 ⊢ ^◡𝑓 ∈ V
38	37	imaex 7958	. . . . . . . . . . 11 ⊢ (^◡𝑓 “ ran 𝐸) ∈ V
39		isfin3-2 10482	. . . . . . . . . . 11 ⊢ ((^◡𝑓 “ ran 𝐸) ∈ V → ((^◡𝑓 “ ran 𝐸) ∈ Fin^III ↔ ¬ ω ≼^* (^◡𝑓 “ ran 𝐸)))
40	38, 39	ax-mp 5	. . . . . . . . . 10 ⊢ ((^◡𝑓 “ ran 𝐸) ∈ Fin^III ↔ ¬ ω ≼^* (^◡𝑓 “ ran 𝐸))
41	40	con2bii 360	. . . . . . . . 9 ⊢ (ω ≼^* (^◡𝑓 “ ran 𝐸) ↔ ¬ (^◡𝑓 “ ran 𝐸) ∈ Fin^III)
42	36, 41	sylib 221	. . . . . . . 8 ⊢ (𝑓:𝐴⟶ontoω → ¬ (^◡𝑓 “ ran 𝐸) ∈ Fin^III)
43		fin1a2lem.aa	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (𝑥 ∈ On ↦ suc 𝑥)
44	12, 43	fin1a2lem6 10520	. . . . . . . . . . . . . 14 ⊢ (𝑆 ↾ ran 𝐸):ran 𝐸⟶1-1onto(ω ∖ ran 𝐸)
45		f1ocnv 6865	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ↾ ran 𝐸):ran 𝐸⟶1-1onto(ω ∖ ran 𝐸) → ^◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)⟶1-1ontoran 𝐸)
46		f1ofo 6860	. . . . . . . . . . . . . 14 ⊢ (^◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)⟶1-1ontoran 𝐸 → ^◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)⟶ontoran 𝐸)
47	44, 45, 46	mp2b 10	. . . . . . . . . . . . 13 ⊢ ^◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)⟶ontoran 𝐸
48		foco 6838	. . . . . . . . . . . . 13 ⊢ ((^◡𝐸:ran 𝐸⟶ontoω ∧ ^◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)⟶ontoran 𝐸) → (^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)⟶ontoω)
49	16, 47, 48	mp2an 705	. . . . . . . . . . . 12 ⊢ (^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)⟶ontoω
50		fofun 6825	. . . . . . . . . . . 12 ⊢ ((^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)⟶ontoω → Fun (^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)))
51	49, 50	ax-mp 5	. . . . . . . . . . 11 ⊢ Fun (^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸))
52	5	resex 6034	. . . . . . . . . . 11 ⊢ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))) ∈ V
53		cofunexg 7993	. . . . . . . . . . 11 ⊢ ((Fun (^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)) ∧ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))) ∈ V) → ((^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)))) ∈ V)
54	51, 52, 53	mp2an 705	. . . . . . . . . 10 ⊢ ((^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)))) ∈ V
55		difss 4075	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ⊆ 𝐴
56	6	fdmd 6748	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴⟶ontoω → dom 𝑓 = 𝐴)
57	55, 56	sseqtrrid 3956	. . . . . . . . . . . . 13 ⊢ (𝑓:𝐴⟶ontoω → (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ⊆ dom 𝑓)
58		fores 6834	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑓 ∧ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ⊆ dom 𝑓) → (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶onto(𝑓 “ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))))
59	22, 57, 58	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝑓:𝐴⟶ontoω → (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶onto(𝑓 “ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))))
60		funcnvcnv 6635	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝑓 → Fun ^◡^◡𝑓)
61		imadif 6652	. . . . . . . . . . . . . . . 16 ⊢ (Fun ^◡^◡𝑓 → (^◡𝑓 “ (ω ∖ ran 𝐸)) = ((^◡𝑓 “ ω) ∖ (^◡𝑓 “ ran 𝐸)))
62	22, 60, 61	3syl 19	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴⟶ontoω → (^◡𝑓 “ (ω ∖ ran 𝐸)) = ((^◡𝑓 “ ω) ∖ (^◡𝑓 “ ran 𝐸)))
63	62	imaeq2d 6068	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴⟶ontoω → (𝑓 “ (^◡𝑓 “ (ω ∖ ran 𝐸))) = (𝑓 “ ((^◡𝑓 “ ω) ∖ (^◡𝑓 “ ran 𝐸))))
64		difss 4075	. . . . . . . . . . . . . . 15 ⊢ (ω ∖ ran 𝐸) ⊆ ω
65		foimacnv 6870	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:𝐴⟶ontoω ∧ (ω ∖ ran 𝐸) ⊆ ω) → (𝑓 “ (^◡𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸))
66	64, 65	mpan2 704	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴⟶ontoω → (𝑓 “ (^◡𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸))
67		fimacnv 6760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓:𝐴⟶ω → (^◡𝑓 “ ω) = 𝐴)
68	6, 67	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:𝐴⟶ontoω → (^◡𝑓 “ ω) = 𝐴)
69	68	difeq1d 4065	. . . . . . . . . . . . . . 15 ⊢ (𝑓:𝐴⟶ontoω → ((^◡𝑓 “ ω) ∖ (^◡𝑓 “ ran 𝐸)) = (𝐴 ∖ (^◡𝑓 “ ran 𝐸)))
70	69	imaeq2d 6068	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝐴⟶ontoω → (𝑓 “ ((^◡𝑓 “ ω) ∖ (^◡𝑓 “ ran 𝐸))) = (𝑓 “ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))))
71	63, 66, 70	3eqtr3rd 2807	. . . . . . . . . . . . 13 ⊢ (𝑓:𝐴⟶ontoω → (𝑓 “ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸))
72		foeq3 6822	. . . . . . . . . . . . 13 ⊢ ((𝑓 “ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸) → ((𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶onto(𝑓 “ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))) ↔ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶onto(ω ∖ ran 𝐸)))
73	71, 72	syl 18	. . . . . . . . . . . 12 ⊢ (𝑓:𝐴⟶ontoω → ((𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶onto(𝑓 “ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))) ↔ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶onto(ω ∖ ran 𝐸)))
74	59, 73	mpbid 235	. . . . . . . . . . 11 ⊢ (𝑓:𝐴⟶ontoω → (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶onto(ω ∖ ran 𝐸))
75		foco 6838	. . . . . . . . . . 11 ⊢ (((^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)⟶ontoω ∧ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶onto(ω ∖ ran 𝐸)) → ((^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶ontoω)
76	49, 74, 75	sylancr 599	. . . . . . . . . 10 ⊢ (𝑓:𝐴⟶ontoω → ((^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶ontoω)
77		fowdom 9600	. . . . . . . . . 10 ⊢ ((((^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)))) ∈ V ∧ ((^◡𝐸 ∘ ^◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (^◡𝑓 “ ran 𝐸))⟶ontoω) → ω ≼^* (𝐴 ∖ (^◡𝑓 “ ran 𝐸)))
78	54, 76, 77	sylancr 599	. . . . . . . . 9 ⊢ (𝑓:𝐴⟶ontoω → ω ≼^* (𝐴 ∖ (^◡𝑓 “ ran 𝐸)))
79		difexg 5296	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ V)
80		isfin3-2 10482	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ V → ((𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III ↔ ¬ ω ≼^* (𝐴 ∖ (^◡𝑓 “ ran 𝐸))))
81	8, 79, 80	3syl 19	. . . . . . . . . 10 ⊢ (𝑓:𝐴⟶ontoω → ((𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III ↔ ¬ ω ≼^* (𝐴 ∖ (^◡𝑓 “ ran 𝐸))))
82	81	con2bid 357	. . . . . . . . 9 ⊢ (𝑓:𝐴⟶ontoω → (ω ≼^* (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ↔ ¬ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III))
83	78, 82	mpbid 235	. . . . . . . 8 ⊢ (𝑓:𝐴⟶ontoω → ¬ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III)
84		eleq1 2852	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝑓 “ ran 𝐸) → (𝑦 ∈ Fin^III ↔ (^◡𝑓 “ ran 𝐸) ∈ Fin^III))
85		difeq2 4060	. . . . . . . . . . . . 13 ⊢ (𝑦 = (^◡𝑓 “ ran 𝐸) → (𝐴 ∖ 𝑦) = (𝐴 ∖ (^◡𝑓 “ ran 𝐸)))
86	85	eleq1d 2849	. . . . . . . . . . . 12 ⊢ (𝑦 = (^◡𝑓 “ ran 𝐸) → ((𝐴 ∖ 𝑦) ∈ Fin^III ↔ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III))
87	84, 86	orbi12d 932	. . . . . . . . . . 11 ⊢ (𝑦 = (^◡𝑓 “ ran 𝐸) → ((𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III) ↔ ((^◡𝑓 “ ran 𝐸) ∈ Fin^III ∨ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III)))
88	87	notbid 321	. . . . . . . . . 10 ⊢ (𝑦 = (^◡𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III) ↔ ¬ ((^◡𝑓 “ ran 𝐸) ∈ Fin^III ∨ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III)))
89		ioran 999	. . . . . . . . . 10 ⊢ (¬ ((^◡𝑓 “ ran 𝐸) ∈ Fin^III ∨ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III) ↔ (¬ (^◡𝑓 “ ran 𝐸) ∈ Fin^III ∧ ¬ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III))
90	88, 89	bitrdi 290	. . . . . . . . 9 ⊢ (𝑦 = (^◡𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III) ↔ (¬ (^◡𝑓 “ ran 𝐸) ∈ Fin^III ∧ ¬ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III)))
91	90	rspcev 3580	. . . . . . . 8 ⊢ (((^◡𝑓 “ ran 𝐸) ∈ 𝒫 𝐴 ∧ (¬ (^◡𝑓 “ ran 𝐸) ∈ Fin^III ∧ ¬ (𝐴 ∖ (^◡𝑓 “ ran 𝐸)) ∈ Fin^III)) → ∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III))
92	11, 42, 83, 91	syl12anc 850	. . . . . . 7 ⊢ (𝑓:𝐴⟶ontoω → ∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III))
93		rexnal 3118	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III) ↔ ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III))
94	92, 93	sylib 221	. . . . . 6 ⊢ (𝑓:𝐴⟶ontoω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III))
95	94	exlimiv 1965	. . . . 5 ⊢ (∃𝑓 𝑓:𝐴⟶ontoω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III))
96	4, 95	sylbi 220	. . . 4 ⊢ (ω ≼^* 𝐴 → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III))
97	96	con2i 140	. . 3 ⊢ (∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III) → ¬ ω ≼^* 𝐴)
98		isfin3-2 10482	. . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin^III ↔ ¬ ω ≼^* 𝐴))
99	97, 98	imbitrrid 249	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III) → 𝐴 ∈ Fin^III))
100	99	imp 412	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ Fin^III ∨ (𝐴 ∖ 𝑦) ∈ Fin^III)) → 𝐴 ∈ Fin^III)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∅c0 4281 𝒫 cpw 4560 class class class wbr 5106 ↦ cmpt 5190 ^◡ccnv 5655 dom cdm 5656 ran crn 5657 ↾ cres 5658 “ cima 5659 ∘ ccom 5660 Oncon0 6386 suc csuc 6388 Fun wfun 6558 ⟶wf 6560 ⟶1-1wf1 6561 ⟶ontowfo 6562 ⟶1-1ontowf1o 6563 (class class class)co 7449 ωcom 7909 2_oc2o 8506 ·_o comu 8510 ≼^* cwdom 9593 Fin^IIIcfin3 10396

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-isom 6573 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-om 7910 df-1st 8033 df-2nd 8034 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-seqom 8494 df-1o 8512 df-2o 8513 df-oadd 8516 df-omul 8517 df-er 8753 df-map 8885 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-wdom 9594 df-card 10055 df-fin4 10402 df-fin3 10403

This theorem is used by: fin1a2lem8 10522

W3C validator