Metamath Proof Explorer


Theorem ssnnfiOLD

Description: Obsolete version of ssnnfi as of 23-Sep-2024. (Contributed by NM, 24-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ssnnfiOLD A ω B A B Fin

Proof

Step Hyp Ref Expression
1 sspss B A B A B = A
2 pssnn A ω B A x A B x
3 elnn x A A ω x ω
4 3 expcom A ω x A x ω
5 4 anim1d A ω x A B x x ω B x
6 5 reximdv2 A ω x A B x x ω B x
7 6 adantr A ω B A x A B x x ω B x
8 2 7 mpd A ω B A x ω B x
9 eleq1 B = A B ω A ω
10 9 biimparc A ω B = A B ω
11 enrefnn B ω B B
12 breq2 x = B B x B B
13 12 rspcev B ω B B x ω B x
14 10 11 13 syl2anc2 A ω B = A x ω B x
15 8 14 jaodan A ω B A B = A x ω B x
16 1 15 sylan2b A ω B A x ω B x
17 isfi B Fin x ω B x
18 16 17 sylibr A ω B A B Fin