Metamath Proof Explorer


Theorem fin1a2lem8

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

Ref Expression
Assertion fin1a2lem8 ( ( ๐ด โˆˆ ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐’ซ ๐ด ( ๐‘ฅ โˆˆ FinIII โˆจ ( ๐ด โˆ– ๐‘ฅ ) โˆˆ FinIII ) ) โ†’ ๐ด โˆˆ FinIII )

Proof

Step Hyp Ref Expression
1 eqid โŠข ( ๐‘ฆ โˆˆ ฯ‰ โ†ฆ ( 2o ยทo ๐‘ฆ ) ) = ( ๐‘ฆ โˆˆ ฯ‰ โ†ฆ ( 2o ยทo ๐‘ฆ ) )
2 eqid โŠข ( ๐‘ฆ โˆˆ On โ†ฆ suc ๐‘ฆ ) = ( ๐‘ฆ โˆˆ On โ†ฆ suc ๐‘ฆ )
3 1 2 fin1a2lem7 โŠข ( ( ๐ด โˆˆ ๐‘‰ โˆง โˆ€ ๐‘ฅ โˆˆ ๐’ซ ๐ด ( ๐‘ฅ โˆˆ FinIII โˆจ ( ๐ด โˆ– ๐‘ฅ ) โˆˆ FinIII ) ) โ†’ ๐ด โˆˆ FinIII )