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

Metamath Proof Explorer

Theorem cflem

Description: A lemma used to simplify cofinality computations, showing the existence of the cardinal of an unbounded subset of a set A . (Contributed by NM, 24-Apr-2004) Avoid ax-11 . (Revised by BTernaryTau, 25-Jul-2025)

Ref Expression
Assertion cflem ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 ssid ⊢ 𝐴 ⊆ 𝐴
2 ssid ⊢ 𝑧 ⊆ 𝑧
3 sseq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑧 ⊆ 𝑤 ↔ 𝑧 ⊆ 𝑧 ) )
4 3 rspcev ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ⊆ 𝑧 ) → ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 )
5 2 4 mpan2 ⊢ ( 𝑧 ∈ 𝐴 → ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 )
6 5 rgen ⊢ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤
7 sseq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
8 rexeq ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) )
9 8 ralbidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) )
10 7 9 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ↔ ( 𝐴 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) ) )
11 10 spcegv ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤 ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
12 1 6 11 mp2ani ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) )
13 fvex ⊢ ( card ‘ 𝑦 ) ∈ V
14 13 isseti ⊢ ∃ 𝑥 𝑥 = ( card ‘ 𝑦 )
15 19.41v ⊢ ( ∃ 𝑥 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ( ∃ 𝑥 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
16 14 15 mpbiran ⊢ ( ∃ 𝑥 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) )
17 16 exbii ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) )
18 fveq2 ⊢ ( 𝑦 = 𝑣 → ( card ‘ 𝑦 ) = ( card ‘ 𝑣 ) )
19 18 eqeq2d ⊢ ( 𝑦 = 𝑣 → ( 𝑥 = ( card ‘ 𝑦 ) ↔ 𝑥 = ( card ‘ 𝑣 ) ) )
20 sseq1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 ⊆ 𝐴 ↔ 𝑣 ⊆ 𝐴 ) )
21 rexeq ⊢ ( 𝑦 = 𝑣 → ( ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ∈ 𝑣 𝑧 ⊆ 𝑤 ) )
22 21 ralbidv ⊢ ( 𝑦 = 𝑣 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑣 𝑧 ⊆ 𝑤 ) )
23 20 22 anbi12d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ↔ ( 𝑣 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑣 𝑧 ⊆ 𝑤 ) ) )
24 19 23 anbi12d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ( 𝑥 = ( card ‘ 𝑣 ) ∧ ( 𝑣 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑣 𝑧 ⊆ 𝑤 ) ) ) )
25 24 excomimw ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
26 17 25 sylbir ⊢ ( ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
27 12 26 syl ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )