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 ‘ 𝑥 ) )