Metamath Proof Explorer


Theorem fin23lem12

Description: The beginning of the proof that every II-finite set (every chain of subsets has a maximal element) is III-finite (has no denumerable collection of subsets).

This first section is dedicated to the construction of U and its intersection. First, the value of U at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis fin23lem.a U=seqωiω,uViftiu=utiurant
Assertion fin23lem12 AωUsucA=iftAUA=UAtAUA

Proof

Step Hyp Ref Expression
1 fin23lem.a U=seqωiω,uViftiu=utiurant
2 1 seqomsuc AωUsucA=Aiω,uViftiu=utiuUA
3 fvex UAV
4 fveq2 i=Ati=tA
5 4 ineq1d i=Atiu=tAu
6 5 eqeq1d i=Atiu=tAu=
7 6 5 ifbieq2d i=Aiftiu=utiu=iftAu=utAu
8 ineq2 u=UAtAu=tAUA
9 8 eqeq1d u=UAtAu=tAUA=
10 id u=UAu=UA
11 9 10 8 ifbieq12d u=UAiftAu=utAu=iftAUA=UAtAUA
12 eqid iω,uViftiu=utiu=iω,uViftiu=utiu
13 3 inex2 tAUAV
14 3 13 ifex iftAUA=UAtAUAV
15 7 11 12 14 ovmpo AωUAVAiω,uViftiu=utiuUA=iftAUA=UAtAUA
16 3 15 mpan2 AωAiω,uViftiu=utiuUA=iftAUA=UAtAUA
17 2 16 eqtrd AωUsucA=iftAUA=UAtAUA