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

Theorem fin1a2lem7 9819
 Description: Lemma for fin1a2 9828. Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014.)
Hypotheses
Ref Expression
fin1a2lem.b 𝐸 = (𝑥 ∈ ω ↦ (2o ·o 𝑥))
fin1a2lem.aa 𝑆 = (𝑥 ∈ On ↦ suc 𝑥)
Assertion
Ref Expression
fin1a2lem7 ((𝐴𝑉 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII)) → 𝐴 ∈ FinIII)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐸
Allowed substitution hints:   𝐴(𝑥)   𝑆(𝑥,𝑦)   𝐸(𝑥)   𝑉(𝑥,𝑦)

Proof of Theorem fin1a2lem7
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 peano1 7583 . . . . . 6 ∅ ∈ ω
2 ne0i 4250 . . . . . 6 (∅ ∈ ω → ω ≠ ∅)
3 brwdomn0 9019 . . . . . 6 (ω ≠ ∅ → (ω ≼* 𝐴 ↔ ∃𝑓 𝑓:𝐴onto→ω))
41, 2, 3mp2b 10 . . . . 5 (ω ≼* 𝐴 ↔ ∃𝑓 𝑓:𝐴onto→ω)
5 vex 3444 . . . . . . . . . 10 𝑓 ∈ V
6 fof 6565 . . . . . . . . . 10 (𝑓:𝐴onto→ω → 𝑓:𝐴⟶ω)
7 dmfex 7625 . . . . . . . . . 10 ((𝑓 ∈ V ∧ 𝑓:𝐴⟶ω) → 𝐴 ∈ V)
85, 6, 7sylancr 590 . . . . . . . . 9 (𝑓:𝐴onto→ω → 𝐴 ∈ V)
9 cnvimass 5916 . . . . . . . . . 10 (𝑓 “ ran 𝐸) ⊆ dom 𝑓
109, 6fssdm 6504 . . . . . . . . 9 (𝑓:𝐴onto→ω → (𝑓 “ ran 𝐸) ⊆ 𝐴)
118, 10sselpwd 5194 . . . . . . . 8 (𝑓:𝐴onto→ω → (𝑓 “ ran 𝐸) ∈ 𝒫 𝐴)
12 fin1a2lem.b . . . . . . . . . . . . . 14 𝐸 = (𝑥 ∈ ω ↦ (2o ·o 𝑥))
1312fin1a2lem4 9816 . . . . . . . . . . . . 13 𝐸:ω–1-1→ω
14 f1cnv 6613 . . . . . . . . . . . . 13 (𝐸:ω–1-1→ω → 𝐸:ran 𝐸1-1-onto→ω)
15 f1ofo 6597 . . . . . . . . . . . . 13 (𝐸:ran 𝐸1-1-onto→ω → 𝐸:ran 𝐸onto→ω)
1613, 14, 15mp2b 10 . . . . . . . . . . . 12 𝐸:ran 𝐸onto→ω
17 fofun 6566 . . . . . . . . . . . 12 (𝐸:ran 𝐸onto→ω → Fun 𝐸)
1816, 17ax-mp 5 . . . . . . . . . . 11 Fun 𝐸
195resex 5866 . . . . . . . . . . 11 (𝑓 ↾ (𝑓 “ ran 𝐸)) ∈ V
20 cofunexg 7634 . . . . . . . . . . 11 ((Fun 𝐸 ∧ (𝑓 ↾ (𝑓 “ ran 𝐸)) ∈ V) → (𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))) ∈ V)
2118, 19, 20mp2an 691 . . . . . . . . . 10 (𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))) ∈ V
22 fofun 6566 . . . . . . . . . . . . 13 (𝑓:𝐴onto→ω → Fun 𝑓)
23 fores 6575 . . . . . . . . . . . . 13 ((Fun 𝑓 ∧ (𝑓 “ ran 𝐸) ⊆ dom 𝑓) → (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→(𝑓 “ (𝑓 “ ran 𝐸)))
2422, 9, 23sylancl 589 . . . . . . . . . . . 12 (𝑓:𝐴onto→ω → (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→(𝑓 “ (𝑓 “ ran 𝐸)))
25 f1f 6549 . . . . . . . . . . . . . . 15 (𝐸:ω–1-1→ω → 𝐸:ω⟶ω)
26 frn 6493 . . . . . . . . . . . . . . 15 (𝐸:ω⟶ω → ran 𝐸 ⊆ ω)
2713, 25, 26mp2b 10 . . . . . . . . . . . . . 14 ran 𝐸 ⊆ ω
28 foimacnv 6607 . . . . . . . . . . . . . 14 ((𝑓:𝐴onto→ω ∧ ran 𝐸 ⊆ ω) → (𝑓 “ (𝑓 “ ran 𝐸)) = ran 𝐸)
2927, 28mpan2 690 . . . . . . . . . . . . 13 (𝑓:𝐴onto→ω → (𝑓 “ (𝑓 “ ran 𝐸)) = ran 𝐸)
30 foeq3 6563 . . . . . . . . . . . . 13 ((𝑓 “ (𝑓 “ ran 𝐸)) = ran 𝐸 → ((𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→(𝑓 “ (𝑓 “ ran 𝐸)) ↔ (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→ran 𝐸))
3129, 30syl 17 . . . . . . . . . . . 12 (𝑓:𝐴onto→ω → ((𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→(𝑓 “ (𝑓 “ ran 𝐸)) ↔ (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→ran 𝐸))
3224, 31mpbid 235 . . . . . . . . . . 11 (𝑓:𝐴onto→ω → (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→ran 𝐸)
33 foco 6577 . . . . . . . . . . 11 ((𝐸:ran 𝐸onto→ω ∧ (𝑓 ↾ (𝑓 “ ran 𝐸)):(𝑓 “ ran 𝐸)–onto→ran 𝐸) → (𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))):(𝑓 “ ran 𝐸)–onto→ω)
3416, 32, 33sylancr 590 . . . . . . . . . 10 (𝑓:𝐴onto→ω → (𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))):(𝑓 “ ran 𝐸)–onto→ω)
35 fowdom 9021 . . . . . . . . . 10 (((𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))) ∈ V ∧ (𝐸 ∘ (𝑓 ↾ (𝑓 “ ran 𝐸))):(𝑓 “ ran 𝐸)–onto→ω) → ω ≼* (𝑓 “ ran 𝐸))
3621, 34, 35sylancr 590 . . . . . . . . 9 (𝑓:𝐴onto→ω → ω ≼* (𝑓 “ ran 𝐸))
375cnvex 7614 . . . . . . . . . . . 12 𝑓 ∈ V
3837imaex 7605 . . . . . . . . . . 11 (𝑓 “ ran 𝐸) ∈ V
39 isfin3-2 9780 . . . . . . . . . . 11 ((𝑓 “ ran 𝐸) ∈ V → ((𝑓 “ ran 𝐸) ∈ FinIII ↔ ¬ ω ≼* (𝑓 “ ran 𝐸)))
4038, 39ax-mp 5 . . . . . . . . . 10 ((𝑓 “ ran 𝐸) ∈ FinIII ↔ ¬ ω ≼* (𝑓 “ ran 𝐸))
4140con2bii 361 . . . . . . . . 9 (ω ≼* (𝑓 “ ran 𝐸) ↔ ¬ (𝑓 “ ran 𝐸) ∈ FinIII)
4236, 41sylib 221 . . . . . . . 8 (𝑓:𝐴onto→ω → ¬ (𝑓 “ ran 𝐸) ∈ FinIII)
43 fin1a2lem.aa . . . . . . . . . . . . . . 15 𝑆 = (𝑥 ∈ On ↦ suc 𝑥)
4412, 43fin1a2lem6 9818 . . . . . . . . . . . . . 14 (𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(ω ∖ ran 𝐸)
45 f1ocnv 6602 . . . . . . . . . . . . . 14 ((𝑆 ↾ ran 𝐸):ran 𝐸1-1-onto→(ω ∖ ran 𝐸) → (𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–1-1-onto→ran 𝐸)
46 f1ofo 6597 . . . . . . . . . . . . . 14 ((𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–1-1-onto→ran 𝐸(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸)
4744, 45, 46mp2b 10 . . . . . . . . . . . . 13 (𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸
48 foco 6577 . . . . . . . . . . . . 13 ((𝐸:ran 𝐸onto→ω ∧ (𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸) → (𝐸(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω)
4916, 47, 48mp2an 691 . . . . . . . . . . . 12 (𝐸(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω
50 fofun 6566 . . . . . . . . . . . 12 ((𝐸(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω → Fun (𝐸(𝑆 ↾ ran 𝐸)))
5149, 50ax-mp 5 . . . . . . . . . . 11 Fun (𝐸(𝑆 ↾ ran 𝐸))
525resex 5866 . . . . . . . . . . 11 (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))) ∈ V
53 cofunexg 7634 . . . . . . . . . . 11 ((Fun (𝐸(𝑆 ↾ ran 𝐸)) ∧ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))) ∈ V) → ((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))) ∈ V)
5451, 52, 53mp2an 691 . . . . . . . . . 10 ((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))) ∈ V
55 difss 4059 . . . . . . . . . . . . . 14 (𝐴 ∖ (𝑓 “ ran 𝐸)) ⊆ 𝐴
566fdmd 6497 . . . . . . . . . . . . . 14 (𝑓:𝐴onto→ω → dom 𝑓 = 𝐴)
5755, 56sseqtrrid 3968 . . . . . . . . . . . . 13 (𝑓:𝐴onto→ω → (𝐴 ∖ (𝑓 “ ran 𝐸)) ⊆ dom 𝑓)
58 fores 6575 . . . . . . . . . . . . 13 ((Fun 𝑓 ∧ (𝐴 ∖ (𝑓 “ ran 𝐸)) ⊆ dom 𝑓) → (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))))
5922, 57, 58syl2anc 587 . . . . . . . . . . . 12 (𝑓:𝐴onto→ω → (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))))
60 funcnvcnv 6391 . . . . . . . . . . . . . . . 16 (Fun 𝑓 → Fun 𝑓)
61 imadif 6408 . . . . . . . . . . . . . . . 16 (Fun 𝑓 → (𝑓 “ (ω ∖ ran 𝐸)) = ((𝑓 “ ω) ∖ (𝑓 “ ran 𝐸)))
6222, 60, 613syl 18 . . . . . . . . . . . . . . 15 (𝑓:𝐴onto→ω → (𝑓 “ (ω ∖ ran 𝐸)) = ((𝑓 “ ω) ∖ (𝑓 “ ran 𝐸)))
6362imaeq2d 5896 . . . . . . . . . . . . . 14 (𝑓:𝐴onto→ω → (𝑓 “ (𝑓 “ (ω ∖ ran 𝐸))) = (𝑓 “ ((𝑓 “ ω) ∖ (𝑓 “ ran 𝐸))))
64 difss 4059 . . . . . . . . . . . . . . 15 (ω ∖ ran 𝐸) ⊆ ω
65 foimacnv 6607 . . . . . . . . . . . . . . 15 ((𝑓:𝐴onto→ω ∧ (ω ∖ ran 𝐸) ⊆ ω) → (𝑓 “ (𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸))
6664, 65mpan2 690 . . . . . . . . . . . . . 14 (𝑓:𝐴onto→ω → (𝑓 “ (𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸))
67 fimacnv 6816 . . . . . . . . . . . . . . . . 17 (𝑓:𝐴⟶ω → (𝑓 “ ω) = 𝐴)
686, 67syl 17 . . . . . . . . . . . . . . . 16 (𝑓:𝐴onto→ω → (𝑓 “ ω) = 𝐴)
6968difeq1d 4049 . . . . . . . . . . . . . . 15 (𝑓:𝐴onto→ω → ((𝑓 “ ω) ∖ (𝑓 “ ran 𝐸)) = (𝐴 ∖ (𝑓 “ ran 𝐸)))
7069imaeq2d 5896 . . . . . . . . . . . . . 14 (𝑓:𝐴onto→ω → (𝑓 “ ((𝑓 “ ω) ∖ (𝑓 “ ran 𝐸))) = (𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))))
7163, 66, 703eqtr3rd 2842 . . . . . . . . . . . . 13 (𝑓:𝐴onto→ω → (𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸))
72 foeq3 6563 . . . . . . . . . . . . 13 ((𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸) → ((𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))) ↔ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)))
7371, 72syl 17 . . . . . . . . . . . 12 (𝑓:𝐴onto→ω → ((𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (𝑓 “ ran 𝐸))) ↔ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)))
7459, 73mpbid 235 . . . . . . . . . . 11 (𝑓:𝐴onto→ω → (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸))
75 foco 6577 . . . . . . . . . . 11 (((𝐸(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω ∧ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)) → ((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→ω)
7649, 74, 75sylancr 590 . . . . . . . . . 10 (𝑓:𝐴onto→ω → ((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→ω)
77 fowdom 9021 . . . . . . . . . 10 ((((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))) ∈ V ∧ ((𝐸(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (𝑓 “ ran 𝐸)))):(𝐴 ∖ (𝑓 “ ran 𝐸))–onto→ω) → ω ≼* (𝐴 ∖ (𝑓 “ ran 𝐸)))
7854, 76, 77sylancr 590 . . . . . . . . 9 (𝑓:𝐴onto→ω → ω ≼* (𝐴 ∖ (𝑓 “ ran 𝐸)))
79 difexg 5195 . . . . . . . . . . 11 (𝐴 ∈ V → (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ V)
80 isfin3-2 9780 . . . . . . . . . . 11 ((𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ V → ((𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII ↔ ¬ ω ≼* (𝐴 ∖ (𝑓 “ ran 𝐸))))
818, 79, 803syl 18 . . . . . . . . . 10 (𝑓:𝐴onto→ω → ((𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII ↔ ¬ ω ≼* (𝐴 ∖ (𝑓 “ ran 𝐸))))
8281con2bid 358 . . . . . . . . 9 (𝑓:𝐴onto→ω → (ω ≼* (𝐴 ∖ (𝑓 “ ran 𝐸)) ↔ ¬ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII))
8378, 82mpbid 235 . . . . . . . 8 (𝑓:𝐴onto→ω → ¬ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII)
84 eleq1 2877 . . . . . . . . . . . 12 (𝑦 = (𝑓 “ ran 𝐸) → (𝑦 ∈ FinIII ↔ (𝑓 “ ran 𝐸) ∈ FinIII))
85 difeq2 4044 . . . . . . . . . . . . 13 (𝑦 = (𝑓 “ ran 𝐸) → (𝐴𝑦) = (𝐴 ∖ (𝑓 “ ran 𝐸)))
8685eleq1d 2874 . . . . . . . . . . . 12 (𝑦 = (𝑓 “ ran 𝐸) → ((𝐴𝑦) ∈ FinIII ↔ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII))
8784, 86orbi12d 916 . . . . . . . . . . 11 (𝑦 = (𝑓 “ ran 𝐸) → ((𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) ↔ ((𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII)))
8887notbid 321 . . . . . . . . . 10 (𝑦 = (𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) ↔ ¬ ((𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII)))
89 ioran 981 . . . . . . . . . 10 (¬ ((𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII) ↔ (¬ (𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII))
9088, 89syl6bb 290 . . . . . . . . 9 (𝑦 = (𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) ↔ (¬ (𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII)))
9190rspcev 3571 . . . . . . . 8 (((𝑓 “ ran 𝐸) ∈ 𝒫 𝐴 ∧ (¬ (𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬ (𝐴 ∖ (𝑓 “ ran 𝐸)) ∈ FinIII)) → ∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
9211, 42, 83, 91syl12anc 835 . . . . . . 7 (𝑓:𝐴onto→ω → ∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
93 rexnal 3201 . . . . . . 7 (∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) ↔ ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
9492, 93sylib 221 . . . . . 6 (𝑓:𝐴onto→ω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
9594exlimiv 1931 . . . . 5 (∃𝑓 𝑓:𝐴onto→ω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
964, 95sylbi 220 . . . 4 (ω ≼* 𝐴 → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII))
9796con2i 141 . . 3 (∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) → ¬ ω ≼* 𝐴)
98 isfin3-2 9780 . . 3 (𝐴𝑉 → (𝐴 ∈ FinIII ↔ ¬ ω ≼* 𝐴))
9997, 98syl5ibr 249 . 2 (𝐴𝑉 → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII) → 𝐴 ∈ FinIII))
10099imp 410 1 ((𝐴𝑉 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴𝑦) ∈ FinIII)) → 𝐴 ∈ FinIII)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∖ cdif 3878   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497   class class class wbr 5030   ↦ cmpt 5110  ◡ccnv 5518  dom cdm 5519  ran crn 5520   ↾ cres 5521   “ cima 5522   ∘ ccom 5523  Oncon0 6159  suc csuc 6161  Fun wfun 6318  ⟶wf 6320  –1-1→wf1 6321  –onto→wfo 6322  –1-1-onto→wf1o 6323  (class class class)co 7135  ωcom 7562  2oc2o 8081   ·o comu 8085   ≼* cwdom 9014  FinIIIcfin3 9694 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-seqom 8069  df-1o 8087  df-2o 8088  df-oadd 8091  df-omul 8092  df-er 8274  df-map 8393  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-wdom 9015  df-card 9354  df-fin4 9700  df-fin3 9701 This theorem is referenced by:  fin1a2lem8  9820
 Copyright terms: Public domain W3C validator