Metamath Proof Explorer


Theorem elfzuzb

Description: Membership in a finite set of sequential integers in terms of sets of upper integers. (Contributed by NM, 18-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion elfzuzb K M N K M N K

Proof

Step Hyp Ref Expression
1 df-3an M K K N M K K N M K K N M K K N
2 an6 M K M K K N K N M K K N M K K N
3 df-3an M N K M N K
4 anandir M N K M K N K
5 an43 M K N K M K K N
6 3 4 5 3bitri M N K M K K N
7 6 anbi1i M N K M K K N M K K N M K K N
8 1 2 7 3bitr4ri M N K M K K N M K M K K N K N
9 elfz2 K M N M N K M K K N
10 eluz2 K M M K M K
11 eluz2 N K K N K N
12 10 11 anbi12i K M N K M K M K K N K N
13 8 9 12 3bitr4i K M N K M N K