This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ x z ⊆ w card ⁡ x

Proof

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