Metamath Proof Explorer

Theorem cfval2

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

Ref Expression
Assertion cfval2 ⊢A∈On→cf⁡A=⋂x∈x∈𝒫A|∀z∈A∃w∈xz⊆wcard⁡x

Proof

Step Hyp Ref Expression
1 cfval ⊢A∈On→cf⁡A=⋂y|∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
2 fvex ⊢card⁡x∈V
3 2 dfiin2 ⊢⋂x∈x∈𝒫A|∀z∈A∃w∈xz⊆wcard⁡x=⋂y|∃x∈x∈𝒫A|∀z∈A∃w∈xz⊆wy=card⁡x
4 df-rex ⊢∃x∈x∈𝒫A|∀z∈A∃w∈xz⊆wy=card⁡x↔∃xx∈x∈𝒫A|∀z∈A∃w∈xz⊆w∧y=card⁡x
5 rabid ⊢x∈x∈𝒫A|∀z∈A∃w∈xz⊆w↔x∈𝒫A∧∀z∈A∃w∈xz⊆w
6 velpw ⊢x∈𝒫A↔x⊆A
7 6 anbi1i ⊢x∈𝒫A∧∀z∈A∃w∈xz⊆w↔x⊆A∧∀z∈A∃w∈xz⊆w
8 5 7 bitri ⊢x∈x∈𝒫A|∀z∈A∃w∈xz⊆w↔x⊆A∧∀z∈A∃w∈xz⊆w
9 8 anbi2ci ⊢x∈x∈𝒫A|∀z∈A∃w∈xz⊆w∧y=card⁡x↔y=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
10 9 exbii ⊢∃xx∈x∈𝒫A|∀z∈A∃w∈xz⊆w∧y=card⁡x↔∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
11 4 10 bitri ⊢∃x∈x∈𝒫A|∀z∈A∃w∈xz⊆wy=card⁡x↔∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
12 11 abbii ⊢y|∃x∈x∈𝒫A|∀z∈A∃w∈xz⊆wy=card⁡x=y|∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
13 12 inteqi ⊢⋂y|∃x∈x∈𝒫A|∀z∈A∃w∈xz⊆wy=card⁡x=⋂y|∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w
14 3 13 eqtr2i ⊢⋂y|∃xy=card⁡x∧x⊆A∧∀z∈A∃w∈xz⊆w=⋂x∈x∈𝒫A|∀z∈A∃w∈xz⊆wcard⁡x
15 1 14 eqtrdi ⊢A∈On→cf⁡A=⋂x∈x∈𝒫A|∀z∈A∃w∈xz⊆wcard⁡x