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 ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } ( card ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 cfval ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) } )
2 fvex ⊢ ( card ‘ 𝑥 ) ∈ V
3 2 dfiin2 ⊢ ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } ( card ‘ 𝑥 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } 𝑦 = ( card ‘ 𝑥 ) }
4 df-rex ⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } 𝑦 = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) )
5 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) )
6 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
7 6 anbi1i ⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) )
8 5 7 bitri ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } ↔ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) )
9 8 anbi2ci ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) ↔ ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) )
10 9 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) ↔ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) )
11 4 10 bitri ⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } 𝑦 = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) )
12 11 abbii ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } 𝑦 = ( card ‘ 𝑥 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) }
13 12 inteqi ⊢ ∩ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } 𝑦 = ( card ‘ 𝑥 ) } = ∩ { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) }
14 3 13 eqtr2i ⊢ ∩ { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) } = ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } ( card ‘ 𝑥 )
15 1 14 eqtrdi ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 } ( card ‘ 𝑥 ) )