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

Metamath Proof Explorer

Theorem cf0

Description: Value of the cofinality function at 0. Exercise 2 of TakeutiZaring p. 102. (Contributed by NM, 16-Apr-2004)

Ref Expression
Assertion cf0 ( cf ‘ ∅ ) = ∅

Proof

Step Hyp Ref Expression
1 cfub ⊢ ( cf ‘ ∅ ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) }
2 0ss ⊢ ∅ ⊆ ∪ 𝑦
3 2 biantru ⊢ ( 𝑦 ⊆ ∅ ↔ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) )
4 ss0b ⊢ ( 𝑦 ⊆ ∅ ↔ 𝑦 = ∅ )
5 3 4 bitr3i ⊢ ( ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ↔ 𝑦 = ∅ )
6 5 anbi1ci ⊢ ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) ↔ ( 𝑦 = ∅ ∧ 𝑥 = ( card ‘ 𝑦 ) ) )
7 6 exbii ⊢ ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 = ∅ ∧ 𝑥 = ( card ‘ 𝑦 ) ) )
8 0ex ⊢ ∅ ∈ V
9 fveq2 ⊢ ( 𝑦 = ∅ → ( card ‘ 𝑦 ) = ( card ‘ ∅ ) )
10 9 eqeq2d ⊢ ( 𝑦 = ∅ → ( 𝑥 = ( card ‘ 𝑦 ) ↔ 𝑥 = ( card ‘ ∅ ) ) )
11 8 10 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = ∅ ∧ 𝑥 = ( card ‘ 𝑦 ) ) ↔ 𝑥 = ( card ‘ ∅ ) )
12 card0 ⊢ ( card ‘ ∅ ) = ∅
13 12 eqeq2i ⊢ ( 𝑥 = ( card ‘ ∅ ) ↔ 𝑥 = ∅ )
14 7 11 13 3bitri ⊢ ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) ↔ 𝑥 = ∅ )
15 14 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) } = { 𝑥 ∣ 𝑥 = ∅ }
16 df-sn ⊢ { ∅ } = { 𝑥 ∣ 𝑥 = ∅ }
17 15 16 eqtr4i ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) } = { ∅ }
18 17 inteqi ⊢ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) } = ∩ { ∅ }
19 8 intsn ⊢ ∩ { ∅ } = ∅
20 18 19 eqtri ⊢ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ ∅ ∧ ∅ ⊆ ∪ 𝑦 ) ) } = ∅
21 1 20 sseqtri ⊢ ( cf ‘ ∅ ) ⊆ ∅
22 ss0b ⊢ ( ( cf ‘ ∅ ) ⊆ ∅ ↔ ( cf ‘ ∅ ) = ∅ )
23 21 22 mpbi ⊢ ( cf ‘ ∅ ) = ∅