Metamath Proof Explorer

Theorem cflim3

Description: Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Hypothesis cflim3.1 ⊢A∈V
Assertion cflim3 ⊢Lim⁡A→cf⁡A=⋂x∈x∈𝒫A|⋃x=Acard⁡x

Proof

Step Hyp Ref Expression
1 cflim3.1 ⊢A∈V
2 limord ⊢Lim⁡A→Ord⁡A
3 1 elon ⊢A∈On↔Ord⁡A
4 2 3 sylibr ⊢Lim⁡A→A∈On
5 cfval ⊢A∈On→cf⁡A=⋂y|∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
6 4 5 syl ⊢Lim⁡A→cf⁡A=⋂y|∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
7 fvex ⊢card⁡x∈V
8 7 dfiin2 ⊢⋂x∈x∈𝒫A|⋃x=Acard⁡x=⋂y|∃x∈x∈𝒫A|⋃x=Ay=card⁡x
9 df-rex ⊢∃x∈x∈𝒫A|⋃x=Ay=card⁡x↔∃xx∈x∈𝒫A|⋃x=A∧y=card⁡x
10 ancom ⊢x∈x∈𝒫A|⋃x=A∧y=card⁡x↔y=card⁡x∧x∈x∈𝒫A|⋃x=A
11 rabid ⊢x∈x∈𝒫A|⋃x=A↔x∈𝒫A∧⋃x=A
12 velpw ⊢x∈𝒫A↔x⊆A
13 12 anbi1i ⊢x∈𝒫A∧⋃x=A↔x⊆A∧⋃x=A
14 coflim ⊢Lim⁡A∧x⊆A→⋃x=A↔∀z∈A∃w∈xz⊆w
15 14 pm5.32da ⊢Lim⁡A→x⊆A∧⋃x=A↔x⊆A∧∀z∈A∃w∈xz⊆w
16 13 15 bitrid ⊢Lim⁡A→x∈𝒫A∧⋃x=A↔x⊆A∧∀z∈A∃w∈xz⊆w
17 11 16 bitrid ⊢Lim⁡A→x∈x∈𝒫A|⋃x=A↔x⊆A∧∀z∈A∃w∈xz⊆w
18 17 anbi2d ⊢Lim⁡A→y=card⁡x∧x∈x∈𝒫A|⋃x=A↔y=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
19 10 18 bitrid ⊢Lim⁡A→x∈x∈𝒫A|⋃x=A∧y=card⁡x↔y=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
20 19 exbidv ⊢Lim⁡A→∃xx∈x∈𝒫A|⋃x=A∧y=card⁡x↔∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
21 9 20 bitrid ⊢Lim⁡A→∃x∈x∈𝒫A|⋃x=Ay=card⁡x↔∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
22 21 abbidv ⊢Lim⁡A→y|∃x∈x∈𝒫A|⋃x=Ay=card⁡x=y|∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
23 22 inteqd ⊢Lim⁡A→⋂y|∃x∈x∈𝒫A|⋃x=Ay=card⁡x=⋂y|∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
24 8 23 eqtr2id ⊢Lim⁡A→⋂y|∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w=⋂x∈x∈𝒫A|⋃x=Acard⁡x
25 6 24 eqtrd ⊢Lim⁡A→cf⁡A=⋂x∈x∈𝒫A|⋃x=Acard⁡x