Metamath Proof Explorer


Theorem coflim

Description: A simpler expression for the cofinality predicate, at a limit ordinal. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion coflim LimABAB=AxAyBxy

Proof

Step Hyp Ref Expression
1 eleq2 B=AxBxA
2 1 biimprd B=AxAxB
3 eluni2 xByBxy
4 limord LimAOrdA
5 ssel2 BAyByA
6 ordelon OrdAyAyOn
7 4 5 6 syl2an LimABAyByOn
8 7 expr LimABAyByOn
9 onelss yOnxyxy
10 8 9 syl6 LimABAyBxyxy
11 10 reximdvai LimABAyBxyyBxy
12 3 11 syl5bi LimABAxByBxy
13 2 12 syl9r LimABAB=AxAyBxy
14 13 ralrimdv LimABAB=AxAyBxy
15 uniss BABA
16 15 3ad2ant2 LimABAxAyBxyBA
17 uniss2 xAyBxyAB
18 17 3ad2ant3 LimABAxAyBxyAB
19 16 18 eqssd LimABAxAyBxyB=A
20 limuni LimAA=A
21 20 3ad2ant1 LimABAxAyBxyA=A
22 19 21 eqtr4d LimABAxAyBxyB=A
23 22 3expia LimABAxAyBxyB=A
24 14 23 impbid LimABAB=AxAyBxy