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)

	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		excom	⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
19	17 18	bitr3i	⊢ ( ∃ 𝑦 ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
20	12 19	sylib	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )