Metamath Proof Explorer

Theorem cflim3

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

Ref Expression
Hypothesis cflim3.1 ⊢ 𝐴 ∈ V
Assertion cflim3 ( Lim 𝐴 → ( cf ‘ 𝐴 ) = ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 cflim3.1 ⊢ 𝐴 ∈ V
2 limord ⊢ ( Lim 𝐴 → Ord 𝐴 )
3 1 elon ⊢ ( 𝐴 ∈ On ↔ Ord 𝐴 )
4 2 3 sylibr ⊢ ( Lim 𝐴 → 𝐴 ∈ On )
5 cfval ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) } )
6 4 5 syl ⊢ ( Lim 𝐴 → ( cf ‘ 𝐴 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) } )
7 fvex ⊢ ( card ‘ 𝑥 ) ∈ V
8 7 dfiin2 ⊢ ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝑥 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) }
9 df-rex ⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) )
10 ancom ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) ↔ ( 𝑦 = ( card ‘ 𝑥 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ) )
11 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) )
12 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
13 12 anbi1i ⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ ∪ 𝑥 = 𝐴 ) )
14 coflim ⊢ ( ( Lim 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( ∪ 𝑥 = 𝐴 ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) )
15 14 pm5.32da ⊢ ( Lim 𝐴 → ( ( 𝑥 ⊆ 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) )
16 13 15 syl5bb ⊢ ( Lim 𝐴 → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) )
17 11 16 syl5bb ⊢ ( Lim 𝐴 → ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ↔ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) )
18 17 anbi2d ⊢ ( Lim 𝐴 → ( ( 𝑦 = ( card ‘ 𝑥 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ) ↔ ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) ) )
19 10 18 syl5bb ⊢ ( Lim 𝐴 → ( ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) ↔ ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) ) )
20 19 exbidv ⊢ ( Lim 𝐴 → ( ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ 𝑦 = ( card ‘ 𝑥 ) ) ↔ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) ) )
21 9 20 syl5bb ⊢ ( Lim 𝐴 → ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) ) )
22 21 abbidv ⊢ ( Lim 𝐴 → { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) } )
23 22 inteqd ⊢ ( Lim 𝐴 → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } = ∩ { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) } )
24 8 23 eqtr2id ⊢ ( Lim 𝐴 → ∩ { 𝑦 ∣ ∃ 𝑥 ( 𝑦 = ( card ‘ 𝑥 ) ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤 ) ) } = ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝑥 ) )
25 6 24 eqtrd ⊢ ( Lim 𝐴 → ( cf ‘ 𝐴 ) = ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝑥 ) )