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 AVxyx=cardyyAzAwyzw

Proof

Step Hyp Ref Expression
1 ssid AA
2 ssid zz
3 sseq2 w=zzwzz
4 3 rspcev zAzzwAzw
5 2 4 mpan2 zAwAzw
6 5 rgen zAwAzw
7 sseq1 y=AyAAA
8 rexeq y=AwyzwwAzw
9 8 ralbidv y=AzAwyzwzAwAzw
10 7 9 anbi12d y=AyAzAwyzwAAzAwAzw
11 10 spcegv AVAAzAwAzwyyAzAwyzw
12 1 6 11 mp2ani AVyyAzAwyzw
13 fvex cardyV
14 13 isseti xx=cardy
15 19.41v xx=cardyyAzAwyzwxx=cardyyAzAwyzw
16 14 15 mpbiran xx=cardyyAzAwyzwyAzAwyzw
17 16 exbii yxx=cardyyAzAwyzwyyAzAwyzw
18 fveq2 y=vcardy=cardv
19 18 eqeq2d y=vx=cardyx=cardv
20 sseq1 y=vyAvA
21 rexeq y=vwyzwwvzw
22 21 ralbidv y=vzAwyzwzAwvzw
23 20 22 anbi12d y=vyAzAwyzwvAzAwvzw
24 19 23 anbi12d y=vx=cardyyAzAwyzwx=cardvvAzAwvzw
25 24 excomimw yxx=cardyyAzAwyzwxyx=cardyyAzAwyzw
26 17 25 sylbir yyAzAwyzwxyx=cardyyAzAwyzw
27 12 26 syl AVxyx=cardyyAzAwyzw