fin34 - Metamath Proof Explorer

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

Theorem fin34 10507

Description: Every III-finite set is IV-finite. (Contributed by Stefan O'Rear, 30-Oct-2014.)

**Assertion**
Ref	Expression
fin34	⊢ (𝐴 ∈ Fin^III → 𝐴 ∈ Fin^IV)

**Proof of Theorem fin34**
Step	Hyp	Ref	Expression
1		isfin3 10413	. . 3 ⊢ (𝐴 ∈ Fin^III ↔ 𝒫 𝐴 ∈ Fin^IV)
2		isfin4-2 10431	. . . . 5 ⊢ (𝒫 𝐴 ∈ Fin^IV → (𝒫 𝐴 ∈ Fin^IV ↔ ¬ ω ≼ 𝒫 𝐴))
3	2	ibi 270	. . . 4 ⊢ (𝒫 𝐴 ∈ Fin^IV → ¬ ω ≼ 𝒫 𝐴)
4		reldom 9017	. . . . . . . 8 ⊢ Rel ≼
5	4	brrelex2i 5715	. . . . . . 7 ⊢ (ω ≼ 𝐴 → 𝐴 ∈ V)
6		canth2g 9188	. . . . . . 7 ⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
7	5, 6	syl 18	. . . . . 6 ⊢ (ω ≼ 𝐴 → 𝐴 ≺ 𝒫 𝐴)
8		domsdomtr 9169	. . . . . 6 ⊢ ((ω ≼ 𝐴 ∧ 𝐴 ≺ 𝒫 𝐴) → ω ≺ 𝒫 𝐴)
9	7, 8	mpdan 700	. . . . 5 ⊢ (ω ≼ 𝐴 → ω ≺ 𝒫 𝐴)
10		sdomdom 9045	. . . . 5 ⊢ (ω ≺ 𝒫 𝐴 → ω ≼ 𝒫 𝐴)
11	9, 10	syl 18	. . . 4 ⊢ (ω ≼ 𝐴 → ω ≼ 𝒫 𝐴)
12	3, 11	nsyl 141	. . 3 ⊢ (𝒫 𝐴 ∈ Fin^IV → ¬ ω ≼ 𝐴)
13	1, 12	sylbi 220	. 2 ⊢ (𝐴 ∈ Fin^III → ¬ ω ≼ 𝐴)
14		isfin4-2 10431	. 2 ⊢ (𝐴 ∈ Fin^III → (𝐴 ∈ Fin^IV ↔ ¬ ω ≼ 𝐴))
15	13, 14	mpbird 260	1 ⊢ (𝐴 ∈ Fin^III → 𝐴 ∈ Fin^IV)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∈ wcel 2147 Vcvv 3454 𝒫 cpw 4560 class class class wbr 5108 ωcom 7911 ≼ cdom 9009 ≺ csdm 9010 Fin^IVcfin4 10397 Fin^IIIcfin3 10398

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 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783

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-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 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-ov 7454 df-om 7912 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-er 8755 df-en 9012 df-dom 9013 df-sdom 9014 df-fin4 10404 df-fin3 10405

This theorem is used by: finngch 10779 infinfnum 35890 fin2so 38798

W3C validator