Metamath Proof Explorer


Theorem fin2i2

Description: A II-finite set contains minimal elements for every nonempty chain. (Contributed by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion fin2i2 AFinIIB𝒫AB[⊂]OrBBB

Proof

Step Hyp Ref Expression
1 simplr AFinIIB𝒫AB[⊂]OrBB𝒫A
2 simpll AFinIIB𝒫AB[⊂]OrBAFinII
3 ssrab2 c𝒫A|AcB𝒫A
4 3 a1i AFinIIB𝒫AB[⊂]OrBc𝒫A|AcB𝒫A
5 simprl AFinIIB𝒫AB[⊂]OrBB
6 fin23lem7 AFinIIB𝒫ABc𝒫A|AcB
7 2 1 5 6 syl3anc AFinIIB𝒫AB[⊂]OrBc𝒫A|AcB
8 sorpsscmpl [⊂]OrB[⊂]Orc𝒫A|AcB
9 8 ad2antll AFinIIB𝒫AB[⊂]OrB[⊂]Orc𝒫A|AcB
10 fin2i AFinIIc𝒫A|AcB𝒫Ac𝒫A|AcB[⊂]Orc𝒫A|AcBc𝒫A|AcBc𝒫A|AcB
11 2 4 7 9 10 syl22anc AFinIIB𝒫AB[⊂]OrBc𝒫A|AcBc𝒫A|AcB
12 sorpssuni [⊂]Orc𝒫A|AcBmc𝒫A|AcBnc𝒫A|AcB¬mnc𝒫A|AcBc𝒫A|AcB
13 9 12 syl AFinIIB𝒫AB[⊂]OrBmc𝒫A|AcBnc𝒫A|AcB¬mnc𝒫A|AcBc𝒫A|AcB
14 11 13 mpbird AFinIIB𝒫AB[⊂]OrBmc𝒫A|AcBnc𝒫A|AcB¬mn
15 psseq2 z=AmwzwAm
16 psseq2 n=AwmnmAw
17 pssdifcom2 mAwAwAmmAw
18 15 16 17 fin23lem11 B𝒫Amc𝒫A|AcBnc𝒫A|AcB¬mnzBwB¬wz
19 1 14 18 sylc AFinIIB𝒫AB[⊂]OrBzBwB¬wz
20 sorpssint [⊂]OrBzBwB¬wzBB
21 20 ad2antll AFinIIB𝒫AB[⊂]OrBzBwB¬wzBB
22 19 21 mpbid AFinIIB𝒫AB[⊂]OrBBB