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 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | โข ( ๐ฆ โ ฯ โฆ ( 2o ยทo ๐ฆ ) ) = ( ๐ฆ โ ฯ โฆ ( 2o ยทo ๐ฆ ) ) | |
2 | eqid | โข ( ๐ฆ โ On โฆ suc ๐ฆ ) = ( ๐ฆ โ On โฆ suc ๐ฆ ) | |
3 | 1 2 | fin1a2lem7 | โข ( ( ๐ด โ ๐ โง โ ๐ฅ โ ๐ซ ๐ด ( ๐ฅ โ FinIII โจ ( ๐ด โ ๐ฅ ) โ FinIII ) ) โ ๐ด โ FinIII ) |