Metamath Proof Explorer


Theorem fin23lem14

Description: Lemma for fin23 . U will never evolve to an empty set if it did not start with one. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis fin23lem.a U=seqωiω,uViftiu=utiurant
Assertion fin23lem14 AωrantUA

Proof

Step Hyp Ref Expression
1 fin23lem.a U=seqωiω,uViftiu=utiurant
2 fveq2 a=Ua=U
3 2 neeq1d a=UaU
4 3 imbi2d a=rantUarantU
5 fveq2 a=bUa=Ub
6 5 neeq1d a=bUaUb
7 6 imbi2d a=brantUarantUb
8 fveq2 a=sucbUa=Usucb
9 8 neeq1d a=sucbUaUsucb
10 9 imbi2d a=sucbrantUarantUsucb
11 fveq2 a=AUa=UA
12 11 neeq1d a=AUaUA
13 12 imbi2d a=ArantUarantUA
14 vex tV
15 14 rnex rantV
16 15 uniex rantV
17 1 seqom0g rantVU=rant
18 16 17 mp1i rantU=rant
19 id rantrant
20 18 19 eqnetrd rantU
21 1 fin23lem12 bωUsucb=iftbUb=UbtbUb
22 21 adantr bωUbUsucb=iftbUb=UbtbUb
23 iftrue tbUb=iftbUb=UbtbUb=Ub
24 23 adantr tbUb=bωUbiftbUb=UbtbUb=Ub
25 simprr tbUb=bωUbUb
26 24 25 eqnetrd tbUb=bωUbiftbUb=UbtbUb
27 iffalse ¬tbUb=iftbUb=UbtbUb=tbUb
28 27 adantr ¬tbUb=bωUbiftbUb=UbtbUb=tbUb
29 neqne ¬tbUb=tbUb
30 29 adantr ¬tbUb=bωUbtbUb
31 28 30 eqnetrd ¬tbUb=bωUbiftbUb=UbtbUb
32 26 31 pm2.61ian bωUbiftbUb=UbtbUb
33 22 32 eqnetrd bωUbUsucb
34 33 ex bωUbUsucb
35 34 imim2d bωrantUbrantUsucb
36 4 7 10 13 20 35 finds AωrantUA
37 36 imp AωrantUA