Metamath Proof Explorer

Theorem cflemOLD

Description: Obsolete version of cflem as of 25-Jul-2025. (Contributed by NM, 24-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cflemOLD ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( 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 ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )