Metamath Proof Explorer

Theorem cflm

Description: Value of the cofinality function at a limit ordinal. Part of Definition of cofinality of Enderton p. 257. (Contributed by NM, 26-Apr-2004)

Ref Expression
Assertion cflm ( ( 𝐴 ∈ 𝐵 ∧ Lim 𝐴 ) → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V )
2 limsuc ⊢ ( Lim 𝐴 → ( 𝑣 ∈ 𝐴 ↔ suc 𝑣 ∈ 𝐴 ) )
3 2 biimpd ⊢ ( Lim 𝐴 → ( 𝑣 ∈ 𝐴 → suc 𝑣 ∈ 𝐴 ) )
4 sseq1 ⊢ ( 𝑧 = suc 𝑣 → ( 𝑧 ⊆ 𝑤 ↔ suc 𝑣 ⊆ 𝑤 ) )
5 4 rexbidv ⊢ ( 𝑧 = suc 𝑣 → ( ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ∈ 𝑦 suc 𝑣 ⊆ 𝑤 ) )
6 5 rspcv ⊢ ( suc 𝑣 ∈ 𝐴 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → ∃ 𝑤 ∈ 𝑦 suc 𝑣 ⊆ 𝑤 ) )
7 sucssel ⊢ ( 𝑣 ∈ V → ( suc 𝑣 ⊆ 𝑤 → 𝑣 ∈ 𝑤 ) )
8 7 elv ⊢ ( suc 𝑣 ⊆ 𝑤 → 𝑣 ∈ 𝑤 )
9 8 reximi ⊢ ( ∃ 𝑤 ∈ 𝑦 suc 𝑣 ⊆ 𝑤 → ∃ 𝑤 ∈ 𝑦 𝑣 ∈ 𝑤 )
10 eluni2 ⊢ ( 𝑣 ∈ ∪ 𝑦 ↔ ∃ 𝑤 ∈ 𝑦 𝑣 ∈ 𝑤 )
11 9 10 sylibr ⊢ ( ∃ 𝑤 ∈ 𝑦 suc 𝑣 ⊆ 𝑤 → 𝑣 ∈ ∪ 𝑦 )
12 6 11 syl6com ⊢ ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → ( suc 𝑣 ∈ 𝐴 → 𝑣 ∈ ∪ 𝑦 ) )
13 3 12 syl9 ⊢ ( Lim 𝐴 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → ( 𝑣 ∈ 𝐴 → 𝑣 ∈ ∪ 𝑦 ) ) )
14 13 ralrimdv ⊢ ( Lim 𝐴 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → ∀ 𝑣 ∈ 𝐴 𝑣 ∈ ∪ 𝑦 ) )
15 dfss3 ⊢ ( 𝐴 ⊆ ∪ 𝑦 ↔ ∀ 𝑣 ∈ 𝐴 𝑣 ∈ ∪ 𝑦 )
16 14 15 imbitrrdi ⊢ ( Lim 𝐴 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → 𝐴 ⊆ ∪ 𝑦 ) )
17 16 adantr ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → 𝐴 ⊆ ∪ 𝑦 ) )
18 uniss ⊢ ( 𝑦 ⊆ 𝐴 → ∪ 𝑦 ⊆ ∪ 𝐴 )
19 limuni ⊢ ( Lim 𝐴 → 𝐴 = ∪ 𝐴 )
20 19 sseq2d ⊢ ( Lim 𝐴 → ( ∪ 𝑦 ⊆ 𝐴 ↔ ∪ 𝑦 ⊆ ∪ 𝐴 ) )
21 18 20 imbitrrid ⊢ ( Lim 𝐴 → ( 𝑦 ⊆ 𝐴 → ∪ 𝑦 ⊆ 𝐴 ) )
22 21 imp ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ∪ 𝑦 ⊆ 𝐴 )
23 17 22 jctird ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → ( 𝐴 ⊆ ∪ 𝑦 ∧ ∪ 𝑦 ⊆ 𝐴 ) ) )
24 eqss ⊢ ( 𝐴 = ∪ 𝑦 ↔ ( 𝐴 ⊆ ∪ 𝑦 ∧ ∪ 𝑦 ⊆ 𝐴 ) )
25 23 24 imbitrrdi ⊢ ( ( Lim 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → 𝐴 = ∪ 𝑦 ) )
26 25 imdistanda ⊢ ( Lim 𝐴 → ( ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) → ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) )
27 26 anim2d ⊢ ( Lim 𝐴 → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ) )
28 27 eximdv ⊢ ( Lim 𝐴 → ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) ) )
29 28 ss2abdv ⊢ ( Lim 𝐴 → { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } )
30 intss ⊢ ( { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
31 29 30 syl ⊢ ( Lim 𝐴 → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
32 31 adantl ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
33 limelon ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ∈ On )
34 cfval ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
35 33 34 syl ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
36 32 35 sseqtrrd ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ⊆ ( cf ‘ 𝐴 ) )
37 cfub ⊢ ( cf ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) }
38 eqimss ⊢ ( 𝐴 = ∪ 𝑦 → 𝐴 ⊆ ∪ 𝑦 )
39 38 anim2i ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) → ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) )
40 39 anim2i ⊢ ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) → ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) )
41 40 eximi ⊢ ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) → ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) )
42 41 ss2abi ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ⊆ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) }
43 intss ⊢ ( { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ⊆ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) } → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) } ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } )
44 42 43 ax-mp ⊢ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) } ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) }
45 37 44 sstri ⊢ ( cf ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) }
46 36 45 jctil ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ( cf ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ∧ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ⊆ ( cf ‘ 𝐴 ) ) )
47 eqss ⊢ ( ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ↔ ( ( cf ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ∧ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } ⊆ ( cf ‘ 𝐴 ) ) )
48 46 47 sylibr ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } )
49 1 48 sylan ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Lim 𝐴 ) → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦 ) ) } )