Metamath Proof Explorer


Theorem elfz2

Description: Membership in a finite set of sequential integers. We use the fact that an operation's value is empty outside of its domain to show M e. ZZ and N e. ZZ . (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion elfz2 K M N M N K M K K N

Proof

Step Hyp Ref Expression
1 anass M N K M K K N M N K M K K N
2 df-3an M N K M N K
3 2 anbi1i M N K M K K N M N K M K K N
4 elfz1 M N K M N K M K K N
5 3anass K M K K N K M K K N
6 ibar M N K M K K N M N K M K K N
7 5 6 syl5bb M N K M K K N M N K M K K N
8 4 7 bitrd M N K M N M N K M K K N
9 fzf : × 𝒫
10 9 fdmi dom = ×
11 10 ndmov ¬ M N M N =
12 11 eleq2d ¬ M N K M N K
13 noel ¬ K
14 13 pm2.21i K M N
15 simpl M N K M K K N M N
16 14 15 pm5.21ni ¬ M N K M N K M K K N
17 12 16 bitrd ¬ M N K M N M N K M K K N
18 8 17 pm2.61i K M N M N K M K K N
19 1 3 18 3bitr4ri K M N M N K M K K N